Packages

package ceres

Content Hierarchy
Ordering
  1. Alphabetic
Visibility
  1. Public
  2. Protected

Type Members

  1. case class A(fo: Formula) extends Struct with Product with Serializable
  2. class CERES extends AnyRef
  3. case class CLS(proof: Expr, config: Sequent[Boolean]) extends Struct with Product with Serializable
  4. class CharacteristicClauseSet extends AnyRef

    Calculates the characteristic clause set

  5. case class Dual(sub: Struct) extends Struct with Product with Serializable
  6. case class EmptyPlusJunction() extends Struct with Product with Serializable
  7. case class EmptyTimesJunction() extends Struct with Product with Serializable
  8. case class Plus(left: Struct, right: Struct) extends Struct with Product with Serializable
  9. 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.

  10. 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
  11. trait StructVisitor[Ret, T] extends AnyRef
  12. case class Times(left: Struct, right: Struct) extends Struct with Product with Serializable

Value Members

  1. object CERES extends CERES

    This implementation of the CERES method does the proof reconstruction via ResolutionToLKProof.

  2. object CharFormN extends StructVisitor[Formula, Unit]
  3. object CharFormP extends StructVisitor[Formula, Unit]
  4. object CharFormPRN
  5. object CharFormPRP
  6. object CharacteristicClauseSet
  7. object DeleteTautology
  8. object InstanceOfSchematicStruct
  9. object InstantiateStruct extends StructVisitor[Struct, (Substitution, Map[CLS, (Struct, Set[Var])], Set[Var])]
  10. 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.

  11. object PlusN
  12. object Projections
  13. object SchematicLeafs
  14. object SchematicStruct
  15. object SimplifyStruct
  16. object SingleProjection
  17. object SingleProjectionWithQuantifiers
  18. object StructCreators
  19. object Times extends Serializable
  20. object Viperize
  21. 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.

  22. object deleteTautologies
  23. object extractStruct
  24. object simpleUnitResolutionNormalization
  25. object subsumedClausesRemoval

Ungrouped