gapt
2.18.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.examples/fol2

fol2

gapt.examples.fol2
object fol2

Provides a simple intuitionistic proof of ¬p ∨ p ⊢ ¬¬p → p. Applying the CERES method will create a non-intuitionistic proof but reductive cut-elimination will always create an intuitionistic one. Therefore this is an example that CERES produces cut-free proofs which reductive cut-elimination cannot.

Attributes

Source
fol2.scala
Graph
Supertypes
class Object
trait Matchable
class Any
Self type
fol2.type

Members list

Value members

Concrete fields

val ax: LogicalAxiom

Attributes

Source
fol2.scala
lazy val ceres_cutfree: LKProof

Attributes

Source
fol2.scala
val cut_left: OrRightRule

Attributes

Source
fol2.scala
val cut_right: ImpRightRule

Attributes

Source
fol2.scala
val p1: NegLeftRule

Attributes

Source
fol2.scala
val p2: NegRightRule

Attributes

Source
fol2.scala
val p3: NegLeftRule

Attributes

Source
fol2.scala
val p4: OrLeftRule

Attributes

Source
fol2.scala
val p5: NegLeftRule

Attributes

Source
fol2.scala
val p6: NegRightRule

Attributes

Source
fol2.scala
val p7: OrLeftRule

Attributes

Source
fol2.scala
val proof: CutRule

Attributes

Source
fol2.scala
lazy val reductive_cutfree: LKProof

Attributes

Source
fol2.scala
Generated with