Type Members

1.  trait Context extends BabelSignature

   Captures constants, types, definitions, and background theory used in a proof.

   Captures constants, types, definitions, and background theory used in a proof.

   Each of these different kinds of information is stored in a separate facet.Facet of the context. Each modification or addition to the context is recorded as an update.Update. Adding information is only possible by adding it as an update.Update. (Basically a Context is an extensible LCF-style kernel.)

   There are several inferences in our LK proofs for which it is not enough that are syntactically valid: An induction inference might follow the syntactical scheme of an induction inference and satisfy the eigenvariable criterion, however if it excludes a constructor of the inductive type, then it still allows us to prove non-theorems. The same is also true for definition rules and theory axioms.

   Hence we store all information necessary to validate these inferences inside a Context object. For completeness, it also includes the collection of constant symbols.

   Having this information available is also important for a second reason: it allows us make decisions based on the current context:

   • The induction tactic uses the information about inductive types to create the necessary subgoals.
   • The Babel parser uses the information about constants to decide whether a free identifier is a variable or a constant, and if it is a constant, what type it should have.
   • The unfold tactic uses the information about definitions to unfold them.
   • The inductive prover can automatically generate random instances for base types.
   • gapt.proofs.expansion.ExpansionProofToLK uses the information about the background theory to produce LK proofs modulo the background theory.
2.  case class ProofDefinition(proofNameTerm: Expr, connector: SequentConnector, proof: LKProof) extends Product with Serializable
3.  class State extends AnyRef

   The state of a context.

   The state of a context.

   A context remembers both its history (what elements were added to it), as well as their effect: the current state (the values of the facets).

   State is basically a Cartesian product of all possible facets, where all except finitely many facets still have their initial value. The get method returns the value of a facet, the update method changes the value.