package proving
The algorithm for proving theorems about MMT content. This is very premature and experimental.
See api for an overview of the algorithms.
The main interfaces are - Prover: object level proving
Structure level proving does not exist yet.
The main implementations are - RuleBasedProver for object-level proving
The latter creates a Searcher for each proving task, which applies search rules to find MMT objects.
- Source
- package.scala
- Alphabetic
- By Inheritance
- proving
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
case class
Alternative(subgoals: List[Goal], proof: () ⇒ Term) extends Product with Serializable
Alternatives are conjunctive goals: an alternative is solved if all its subgoals are.
Alternatives are conjunctive goals: an alternative is solved if all its subgoals are.
- subgoals
the conjuncts of this alternative
- proof
returns the proof term (to be called only if
isSolved == true) When instantiating this class, proof may call the corresponding method of each subgoal.
-
abstract
class
ApplicableTactic extends AnyRef
a continuation function returned by a Tactic to be run if the tactic is to be applied
a continuation function returned by a Tactic to be run if the tactic is to be applied
A tactic may return multiple continuations if it is applicable in multiple different ways. Low-priority tactics may move expensive computations into the continuation to avoid unnecessary work
-
case class
Atom(tm: Term, tp: Term, rl: Option[String]) extends Product with Serializable
an atomic fact: a constant or a variable
an atomic fact: a constant or a variable
- tm
the proof term
- tp
the proved type
-
case class
AtomicShape(term: Term) extends Shape with Product with Serializable
a leaf representing an atomic subterm (constant, outer variable, literal)
-
trait
BackwardInvertible extends InvertibleTactic
an InvertibleTactic, whose behavior depends only on the conclusion of a goal
-
trait
BackwardSearch extends Tactic
a backward tactic generates additional ways to reach the goal
a backward tactic generates additional ways to reach the goal
This is used in backward proof search
-
case class
BoundShape(index: Int) extends Shape with Product with Serializable
a leaf representing a variable bound by a governing ComplexShape
-
case class
ComplexShape(op: GlobalName, children: List[Shape]) extends Shape with Product with Serializable
a non-replaced node in the syntax/shape tree, variable bindings are approximated by the shape of the type
-
class
EquivalenceClass extends ShapeIndexedSet[Term]
class in an EquivalenceRelation
-
class
EquivalenceRelation extends AnyRef
a container for relations like ==, !=, and <= on terms which are indexed by shape)
a container for relations like ==, !=, and <= on terms which are indexed by shape)
the class approximates the relations based on the available knowledge initially nothing is known, and instances are added over time
knowledge grows monotonously and cannot be removed inconsistency can arise (which can, e.g., be used to terminate a proof)
the class implements - reflexivity, symmetry, and (cached) transitivity of == - irreflexivity and symmetry of != - reflexivity, anti-symmetry wrt ==, and (not cached) transitivity of <= - congruence of <= wrt == - disjointness of == and != (used to detect inconsistency)
-
case class
Fact(goal: Goal, tm: Term, tp: Term) extends Product with Serializable
a fact is a sequent derived during forward search
a fact is a sequent derived during forward search
- goal
antecedent of the fact (conclusion of the goal is irrelevant)
- tm
the proof term
- tp
the proved type
-
class
Facts extends Logger
A database of facts obtained through forward proof search
-
trait
ForwardInvertible extends InvertibleTactic
an InvertibleTactic, whose behavior depends only on the context of a goal
-
trait
ForwardSearch extends Tactic
a forward tactic generates additional facts that are implied by the assumptions
a forward tactic generates additional facts that are implied by the assumptions
This is used in forward proof search
-
class
Goal extends AnyRef
A Goal is a single-conclusion sequent - the basic node in a proof tree.
A Goal is a single-conclusion sequent - the basic node in a proof tree. A goal nodes knows its parent (except for the root goal) and children (the alternatives and their subgoals).
Each Goal stores a partial proof: a list of alternatives each of which stores a list of subgoals. Goals are disjunctive: a goal can be closed if all subgoals of one alternative can be closed.
The conclusion, the proof alternatives, and the proof term are stored statefully and are set by this class or other prover components.
The prover expands new goals greedily by applying invertible rules, and each goal stores those invertible rules that have not been applied yet.
-
trait
InvertibleTactic extends Tactic
invertible tactics can be applied greedily without leading a proof into a dead end
invertible tactics can be applied greedily without leading a proof into a dead end
this type includes both invertible forward (e.g., existential elimination) and backwards rules (e.g., universal introduction)
-
abstract
class
Prover extends Extension
A prover conducts the proof search.
-
case class
ProvingUnit(component: Option[CPath], context: Context, tp: Term, logPrefix: String) extends MMTTask with Product with Serializable
represents a proof obligation
represents a proof obligation
- component
the URI of the declaration component that triggered this proof obligation
- context
the left-hand side/antecedent, i.e., the global (via IncludeVarDecl) and local (via VarDecl) assumptions
- tp
the type to be inhabited, i.e., the right-hand side/succedent, i.e., the proof goal
- logPrefix
the log prefix to use
-
class
RuleBasedProver extends Prover
a simple prover
-
class
Searcher extends Logger
Conducts proof search, e.g., as used by the RuleBasedProver.
Conducts proof search, e.g., as used by the RuleBasedProver. A new instance must be created for each proof obligation.
-
abstract
class
Shape extends AnyRef
an approximation of the syntax tree of a Term that replaces subtrees beyond a certain depth with special leaves
an approximation of the syntax tree of a Term that replaces subtrees beyond a certain depth with special leaves
Shapes can be used as keys when indexing sets of terms, as in Facts
-
class
ShapeIndexedSet[A] extends ComplexHashSet[Shape, A]
a hash set using shapes of a certain height as keys
-
trait
Tactic extends SyntaxDrivenRule
A rule used for forward or backward proof search