package proof
- Alphabetic
- Public
- Protected
Package Members
- package certificates
- package goal
- package theoryPlugins
- package tree
Type Members
- case class BindingContext extends PartialOrdering[ConstantTerm] with Product with Serializable
Class to represent the context of constants bound above a certain node in the proof tree.
Class to represent the context of constants bound above a certain node in the proof tree. This constant can be seen as a partial ordering on constants: inner bound constants are bigger than outer bound constants
- class ConstantFreedom extends PartiallyOrdered[ConstantFreedom]
Class to represent the set of constants that are considered as "free" (i.e., that are only unifiable with themselves).
Class to represent the set of constants that are considered as "free" (i.e., that are only unifiable with themselves). Objects of this class are stored in the nodes of proof tree and are updated when the proof is expanded in order to eventually reach a fixed point.
TODO: avoid the creation of new objects whenever possible
- abstract class ConstraintSimplifier extends AnyRef
- class ExhaustiveProver extends AnyRef
A prover that tries to construct an exhaustive proof for a given goal.
A prover that tries to construct an exhaustive proof for a given goal. The prover tries to optimise by early stopping the expansion of the proof tree if it is detected that a certain subtree can never yield a satisfiable closing constraint. There are two main modes of operation: with
depthFirst, it is tried to derive a satisfiable constraint from the given problem, without aiming for exhaustiveness. Without this option, the tree is expanded depth-first until it is exhaustive (which terminates in the case of PA formulae, but not in general). - class ModelSearchProver extends AnyRef
A prover that tries to construct a countermodel of a ground formula.
A prover that tries to construct a countermodel of a ground formula. This prover works in depth-first mode, in contrast to the
ExhaustiveProver. - class SimpleSimplifier extends ConstraintSimplifier
- case class Vocabulary(order: TermOrder, bindingContext: BindingContext, constantFreedom: ConstantFreedom) extends Product with Serializable
Value Members
- object BindingContext extends Serializable
- object ConstantFreedom
- object ConstraintSimplifier
- object ExhaustiveProver
- object ModelSearchProver
A prover that tries to construct a countermodel of a ground formula.
A prover that tries to construct a countermodel of a ground formula. This prover works in depth-first mode, in contrast to the
ExhaustiveProver. - object QuantifierElimProver
Prover to eliminate quantifiers in a PA formula.
Prover to eliminate quantifiers in a PA formula. The prover is losely based on the idea in the paper "A Quantifier Elimination Algorithm for Linear Real Arithmetic" by David Monniaux, although it does not explicitly compute solutions of the matrix of a quantified formula like in the paper. Instead, the constraint extracted from an exhaustive subtree is injected as a lemma into other subtrees and used to close such subtrees earlier.
It is assumed that it is never necessary to adjust the constant freedom of a proof tree in this setting, because all constants that shield formulas also have to be eliminated constants and, thus, never occur in constraints anyway. This makes it possible to construct proof trees in a purely depth-first way (just like in the
ModelSearchProver)TODO: at the moment, this prover does not support theories like bit-vectors or multiplication
- object Vocabulary extends Serializable