proof

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
package certificates
package goal
package theoryPlugins
package tree

package proof

Type Members

case class BindingContext extends PartialOrdering[ConstantTerm] with Product with Serializable

class ConstantFreedom extends PartiallyOrdered[ConstantFreedom]

abstract class ConstraintSimplifier extends AnyRef

class ExhaustiveProver extends AnyRef

class ModelSearchProver extends AnyRef

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

object QuantifierElimProver

object Vocabulary extends Serializable

package certificates

package goal

package theoryPlugins

package tree

Ungrouped