Package

ap

proof

Permalink

package proof

Visibility
  1. Public
  2. All

Type Members

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

    Permalink

    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

  2. class ConstantFreedom extends PartiallyOrdered[ConstantFreedom]

    Permalink

    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

  3. abstract class ConstraintSimplifier extends AnyRef

    Permalink
  4. class ExhaustiveProver extends AnyRef

    Permalink

    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).

  5. class ModelSearchProver extends AnyRef

    Permalink

    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.

  6. class SimpleSimplifier extends ConstraintSimplifier

    Permalink
  7. class TestEquationSystems extends APTestCase

    Permalink
  8. class TestRandomProving extends APTestCase

    Permalink
  9. case class Vocabulary(order: TermOrder, bindingContext: BindingContext, constantFreedom: ConstantFreedom) extends Product with Serializable

    Permalink

Value Members

  1. object BindingContext extends Serializable

    Permalink
  2. object ConstantFreedom

    Permalink
  3. object ConstraintSimplifier

    Permalink
  4. object ExhaustiveProver

    Permalink
  5. object ModelSearchProver

    Permalink

    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.

  6. object QuantifierElimProver

    Permalink

    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

  7. object Vocabulary extends Serializable

    Permalink
  8. package certificates

    Permalink
  9. package goal

    Permalink
  10. package theoryPlugins

    Permalink
  11. package tree

    Permalink

Ungrouped