Class and Description |
---|
Node |
NodeInfo
The node info object contains additional information about a node used to
give user feedback.
|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
ProofAggregate |
ProofEvent
an object indicating that a proof event has happpend
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
MissingInstantiationException |
ModelChangeListener
this interface is implemented by listener of change
events of a model
|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
SVInstantiationException |
SVInstantiationParserException |
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
ProofAggregate |
ProofEvent
an object indicating that a proof event has happpend
|
Class and Description |
---|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Class and Description |
---|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Node |
Class and Description |
---|
Node |
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
BuiltInRuleIndex
Index for managing built-in-rules usch as integer decision or update
simplification rule.
|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Statistics
Instances of this class encapsulate statistical information about proofs,
such as the number of nodes, or the number of interactions.
|
TacletIndex
manages all applicable Taclets (more precisely: Taclets with
instantiations but without position information, the NoPosTacletApps)
at one node.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Counter
Proof-specific counter object: taclet names, var names, node numbers, &c
|
JavaModel |
NameRecorder |
Node |
PrefixTermTacletAppIndexCacheImpl.CacheKey |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
TermProgramVariableCollector |
TermTacletAppIndex
Class whose objects represent an index of taclet apps for one particular
position within a formula, and that also contain references to the indices of
direct subformulas
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
InstantiationProposer
Provides proposals for schema variable instantiations.
|
Node |
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
BuiltInRuleAppIndex |
BuiltInRuleIndex
Index for managing built-in-rules usch as integer decision or update
simplification rule.
|
Counter
Proof-specific counter object: taclet names, var names, node numbers, &c
|
FormulaTag
Class whose instances represent tags to identify the formulas of sequents
persistently, i.e.
|
FormulaTagManager
Class to manage the tags of the formulas of a sequent (node).
|
Goal
A proof is represented as a tree of nodes containing sequents.
|
GoalListener
interface to be implemented by a goal listener
|
InstantiationProposer
Provides proposals for schema variable instantiations.
|
ITermTacletAppIndexCache
The general interface for caches for accelerating
TermTacletAppIndex . |
JavaModel |
ModelEvent
this class represents a Model event
|
NameRecorder |
NewRuleListener
Interface for tracking new RuleApps
|
Node |
NodeInfo
The node info object contains additional information about a node used to
give user feedback.
|
PrefixTermTacletAppIndexCacheImpl
The abstract superclass of caches for taclet app indexes that are implemented
using a common backend
LRUCache (the backend is stored in
TermTacletAppIndexCacheSet ). |
PrefixTermTacletAppIndexCacheImpl.CacheKey |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
ProofAggregate |
ProofEvent
an object indicating that a proof event has happpend
|
ProofTreeEvent
Encapsulates information describing changes to a proof tree, and
used to notify proof tree listeners of the change.
|
ProofTreeListener |
ProofVisitor |
ReplacementMap
A map to be used in an
OpReplacer . |
RuleAppIndex
manages the possible application of rules (RuleApps)
|
RuleAppListener
This listener is notified whenever a rule is applied in an ongoing proof.
|
SemisequentTacletAppIndex
This class holds
TermTacletAppIndex s for all formulas of
a semisequent. |
Statistics
Instances of this class encapsulate statistical information about proofs,
such as the number of nodes, or the number of interactions.
|
StrategyInfoUndoMethod |
SVInstantiationException |
SVInstantiationExceptionWithPosition
Represents an exception with position information.
|
SVInstantiationParserException |
TacletAppIndex
the class manages the available TacletApps.
|
TacletIndex
manages all applicable Taclets (more precisely: Taclets with
instantiations but without position information, the NoPosTacletApps)
at one node.
|
TacletIndexKit
Abstract factory for creating
TacletIndex instances |
TermProgramVariableCollector |
TermTacletAppIndex
Class whose objects represent an index of taclet apps for one particular
position within a formula, and that also contain references to the indices of
direct subformulas
|
TermTacletAppIndexCacheSet
Cache that is used for accelerating
TermTacletAppIndex . |
VariableNameProposer
Proposes names for variables (except program variables).
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
BuiltInRuleIndex
Index for managing built-in-rules usch as integer decision or update
simplification rule.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
ProofAggregate |
TacletIndex
manages all applicable Taclets (more precisely: Taclets with
instantiations but without position information, the NoPosTacletApps)
at one node.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
ProofAggregate |
Class and Description |
---|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
JavaModel |
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
ProofAggregate |
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
GoalListener
interface to be implemented by a goal listener
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Node |
Class and Description |
---|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
NewRuleListener
Interface for tracking new RuleApps
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
NodeInfo
The node info object contains additional information about a node used to
give user feedback.
|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Node |
NodeInfo
The node info object contains additional information about a node used to
give user feedback.
|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
NodeInfo
The node info object contains additional information about a node used to
give user feedback.
|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Class and Description |
---|
Node |
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
ProofAggregate |
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
ProofAggregate |
ProofEvent
an object indicating that a proof event has happpend
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
ProofAggregate |
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
ProofEvent
an object indicating that a proof event has happpend
|
Class and Description |
---|
Node |
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Proof
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
Class and Description |
---|
Goal
A proof is represented as a tree of nodes containing sequents.
|
Node |
Copyright © 2003-2019 The KeY-Project.