package ceres
- Alphabetic
- Public
- Protected
Type Members
- case class A(fo: Formula) extends Struct with Product with Serializable
- class CERES extends AnyRef
- case class CLS(proof: Expr, config: Sequent[Boolean]) extends Struct with Product with Serializable
- class CharacteristicClauseSet extends AnyRef
Calculates the characteristic clause set
- case class Dual(sub: Struct) extends Struct with Product with Serializable
- case class EmptyPlusJunction() extends Struct with Product with Serializable
- case class EmptyTimesJunction() extends Struct with Product with Serializable
- case class Plus(left: Struct, right: Struct) extends Struct with Product with Serializable
- trait Struct extends AnyRef
The superclass for all struct elements: atom, negated atom, junction, times and the neutral elememts for the latter two.
The superclass for all struct elements: atom, negated atom, junction, times and the neutral elememts for the latter two. For details refer to Bruno Woltzenlogel-Paleo's PhD Thesis.
- case class StructTransformer[Ret, T](aF: (Formula, T) => Ret, pF: (Ret, Ret, T) => Ret, pD: Ret, tF: (Ret, Ret, T) => Ret, tD: Ret, dF: (Ret, T) => Ret, cF: (Expr, Sequent[Boolean], T) => Ret) extends Product with Serializable
- trait StructVisitor[Ret, T] extends AnyRef
- case class Times(left: Struct, right: Struct) extends Struct with Product with Serializable
Value Members
- object CERES extends CERES
This implementation of the CERES method does the proof reconstruction via ResolutionToLKProof.
- object CharFormN extends StructVisitor[Formula, Unit]
- object CharFormP extends StructVisitor[Formula, Unit]
- object CharFormPRN
- object CharFormPRP
- object CharacteristicClauseSet
- object DeleteTautology
- object InstanceOfSchematicStruct
- object InstantiateStruct extends StructVisitor[Struct, (Substitution, Map[CLS, (Struct, Set[Var])], Set[Var])]
- object Pickrule
The pick* functions generalize the convenience constructors of the LK rules which allow to specify arguments by a formula instead of an index.
The pick* functions generalize the convenience constructors of the LK rules which allow to specify arguments by a formula instead of an index. Here we lookup fitting matches for the auxiliary formulas of each LK rule. In the case of LK, fitting is defined as equality of the formula. In the case of LKsk, it is equality of formulas and skolem symbols. An algorithm using pickrule is therefore easier to transfer to LKsk.
- object PlusN
- object Projections
- object SchematicLeafs
- object SchematicStruct
- object SimplifyStruct
- object SingleProjection
- object SingleProjectionWithQuantifiers
- object StructCreators
- object Times extends Serializable
- object Viperize
- object coloredStructString
Returns s.toString with color coding of struct operators.
Returns s.toString with color coding of struct operators. When a big struct is loaded in the cli, the string truncation can mess up the terminal, therefore this is not the default behaviour.
- object deleteTautologies
- object extractStruct
- object simpleUnitResolutionNormalization
- object subsumedClausesRemoval
This is the API documentation for GAPT.
The main package is gapt.