PredicateReductionCNF
gapt.proofs.reduction.PredicateReductionCNF
case object PredicateReductionCNF extends Reduction_[Set[HOLClause], ResolutionProof]
Simplifies the problem of finding a resolution refutation of a many-sorted clause set by adding predicates for each of the sorts. The resulting problem is still many-sorted.
Attributes
- Source
- manySorted.scala
- Graph
-
- Supertypes
- Self type
Members list
Type members
Inherited types
The names of the product elements
Attributes
- Inherited from:
- Singleton
- Source
- Mirror.scala
The mirrored *-type
Attributes
- Inherited from:
- Singleton
- Source
- Mirror.scala
Inherited and Abstract types
The name of the type
Value members
Concrete methods
Attributes
- Definition Classes
- Source
- manySorted.scala
Inherited methods
Create a new instance of type T with elements taken from product p.
Create a new instance of type T with elements taken from product p.
Attributes
- Inherited from:
- Singleton
- Source
- Mirror.scala
Attributes
- Inherited from:
- Product
Attributes
- Inherited from:
- Product
def |>[P2_ >: Set[HOLClause], P3, S2_ <: ResolutionProof, S3](other: Reduction[P2_, P3, S2_, S3]): Reduction[Set[HOLClause], P3, ResolutionProof, S3]
Sequentially composes reductions.
In this article