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