CNFReductionResRes
gapt.proofs.reduction.CNFReductionResRes
case object CNFReductionResRes extends Reduction[HOLSequent, Set[HOLClause], ResolutionProof, ResolutionProof]
Reduces finding a resolution proof for a sequent to finding a resolution proof of a clause set.
Attributes
- Source
- manySorted.scala
- Graph
-
- Supertypes
- Self type
-
CNFReductionResRes.type
Members list
Type members
Inherited types
The names of the product elements
Attributes
- Inherited from:
- Singleton
- Source
- Mirror.scala
The name of the type
The mirrored *-type
Attributes
- Inherited from:
- Singleton
- Source
- Mirror.scala
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
Sequentially composes reductions.
In this article