Inference corresponding to an application of alpha rules.
Turn two complementary inequalities into an equation
Certificate corresponding to an application of beta rules with lemmas: the
rule describes the splitting of an antecedent formula
leftFormula | rightFormula
into the cases
leftFormula
and !leftFormula, rightFormula
.
Abstract superclass of certificates with two children
Abstract superclass of all inferences that do not cause proof splitting and that do not close proof branches
Inferences that do not cause proof splitting and that do not close a branch are collected in nodes of this class.
Class to store sets of branch inferences in goals.
Class to store sets of branch inferences in goals. Currently, the inferences
are just kept in a list, but this might change at a late point. This is an
immutable datastructure, for dynamically collecting inferences use
BranchInferenceCollector
.
Compound formulae in certificates
Formula expressing an equation lhs = 0
Formula expressing an equation lhs = 0
Hierarchy of formulae specifically for representing certificates; the reason is that the standard formula datastructures perform too much simplification implicitly
Formula expressing an inequality lhs >= 0
Formula expressing an inequality lhs >= 0
Formula expressing a negated equation lhs != 0
Formula expressing a negated equation lhs != 0
Formula expressing a positive or negative occurrence of a predicate atom
Datastructures used to express and extract whole, detailed proofs, which can independently be checked and be used for further processing (e.g., to compute interpolants).
Datastructures used to express and extract whole, detailed proofs, which can independently be checked and be used for further processing (e.g., to compute interpolants). Certificates are trees/proof terms, with the following class as the abstract superclass of all tree nodes. Proofs are more or less tableau proofs, with rule applications assuming certain formulae on a branch and producing new formulae.
Abstract superclass of all certificate nodes that only have a single subtree
Certificate corresponding to an application of the close rule.
Inference corresponding to an application of the col-red
or
col-red-subst
rule.
Inference corresponding to an application of the col-red
or
col-red-subst
rule. This will simply introduce a new constant
newSymbol
that is defined by definingEquation
.
Inference corresponding to a series of applications of the reduce rule: form the linear combination of a sequence of equations.
Inference corresponding to a series of applications of the reduce rule: form the linear combination of a sequence of equations. The result is implicitly made primitive (divided by common coefficients)
Inference corresponding to a series of applications of the reduce rule: form the linear combination of a sequence of equations.
Inference corresponding to a series of applications of the reduce rule: form the linear combination of a sequence of equations. The result is implicitly made primitive (divided by common coefficients) and rounded
Class for converting a given certificate to a DAG, by factoring out shared sub-certificates.
Given the two formulae t >= 0
and t != 0
(or,
similarly, t >= 0
and -t != 0
), infer
the inequality t-1 >= 0
.
Given the two formulae t >= 0
and t != 0
(or,
similarly, t >= 0
and -t != 0
), infer
the inequality t-1 >= 0
. This kind of inference exists as a
separate rule to keep certificates more compact.
An inference that turns a universally quantified divisibility constraint into an existentially quantified conjunction of inequalities and an equation.
Class for dumping a certificate in the dot/GraphViz format
Inference corresponding to applications of the rules all-left
,
ex-left
, etc.
Inference corresponding to applications of the rules all-left
,
ex-left
, etc. A uniform prefix of quantifiers (only forall or
only exists) is instantiated with a single inference.
newConstants
are the constants introduced to instantiate the
quantifiers, starting with the innermost instantiated quantifier.
Mutable class for managing sets of certificates.
Mutable datastructure for collecting inferences during some computation.
Mutable datastructure for collecting inferences during some computation. To avoid having to pass around collectors all over the place, a dynamic variable is used to realise context collectors.
An inference encapsulating multiple inferences, to be expanded on demand.
Certificate corresponding to an application of the Omega rule, which has the
same effect as repeated application of Strengthen to the inequalities
boundsA
in a goal.
Certificate corresponding to an application of the Omega rule, which has the
same effect as repeated application of Strengthen to the inequalities
boundsA
in a goal.
For each of the inequalities in boundsA
,
strengthenCases
tells how often
Strengthen is applied. The counting works just like in
StrengthenCertificate
, i.e., 1
means that
Strenghten is applied once (and there are two cases).
Class representing a mapping from a vector of certificates to a single new certificate.
Class representing a mapping from a vector of certificates to a single new certificate. This is used to handle certificate extraction in branching proofs.
An inference encapsulating the application of a unary
PartialCertificate
.
An inference encapsulating the application of a unary
PartialCertificate
.
Partial certificate representing branching proof nodes.
Composition of a partial certificate and a sequence of partial certificates.
A partial certificate with a fixed result.
Partial certificate prepending given inferences to some certificate.
An inference describing the unification of two predicates, producing a system of equations (in the succedent) that express the unification conditions: the predicate arguments are matched pair-wise
Inference corresponding to applications of the rules all-left
,
ex-left
, etc.
Inference corresponding to applications of the rules all-left
,
ex-left
, etc. A uniform prefix of quantifiers (only forall or
only exists) is instantiated with a single inference.
newConstants
are the constants introduced to instantiate the
quantifiers, starting with the innermost instantiated quantifier.
Inference corresponding to a series of applications of the reduce rule to a
negated equation or an inequality (reduction of positive equalities is
described using CombineEquationsInference
).
Inference corresponding to a series of applications of the reduce rule to a
negated equation or an inequality (reduction of positive equalities is
described using CombineEquationsInference
).
Inference corresponding to a series of applications of the reduce rule to the arguments of a predicate literal.
Inference corresponding to a series of applications of the reduce rule to the
arguments of a predicate literal. This is essentially the same as the
ReduceInference
, only that all of the arguments can be reduced
simultaneously
Inference representing the simplification of an equation, a negated equation, or an inequality
Certificate corresponding to splitting a negated equation into two inequalities.
Certificate corresponding to a (possibly repeated) application of the
strengthen rule: the inequality weakInEq(0) >= 0
is strengthened
to the equations weakInEq(0) === 0
,
weakInEq(0) === 1
, etc.
Certificate corresponding to a (possibly repeated) application of the
strengthen rule: the inequality weakInEq(0) >= 0
is strengthened
to the equations weakInEq(0) === 0
,
weakInEq(0) === 1
, etc. and the inequality
weakInEq(0) >= eqCases
.
An inference describing the introduction of a theory axiom.
Partial certificate that represents the identify function.
Inference marking that the following sub-proof has been reused from a previous point.
Certificate corresponding to an application of beta rules with lemmas: the rule describes the splitting of an antecedent formula
leftFormula | rightFormula
into the casesleftFormula
and!leftFormula, rightFormula
. (Iflemma
is not set, the second case is justrightFormula
)