gapt.proofs.lk.transformations.LKToND
Attributes
- Source
-
LKToND.scala
- Graph
-
- Supertypes
-
class Object
trait Matchable
class Any
- Self type
-
Members list
Converts an LKProof π into a natural deduction proof.
Converts an LKProof π into a natural deduction proof.
Value parameters
- focus
-
The index in the LK succedent of the formula to be proved in the ND proof, or None if the succedent is empty.
- proof
-
The proof π.
Attributes
- Returns
-
The natural deduction proof translate(π).
- Source
-
LKToND.scala