kolmogorov
Attributes
- Source
- transformation.scala
- Graph
-
- Supertypes
-
class Objecttrait Matchableclass Any
- Self type
-
kolmogorov.type
Members list
Value members
Concrete methods
Applies the Kolmogorov proof transformation to a given natural deduction proof. The transformation removes all occurences of the excluded middle rule and the botttom elimination rule, and thus the resulting proof is a proof in intuitionistic, minimal logic. The conclusion of the resulting proof is the Kolmogorov trnaslation k applied to the original conclusion.
Applies the Kolmogorov proof transformation to a given natural deduction proof. The transformation removes all occurences of the excluded middle rule and the botttom elimination rule, and thus the resulting proof is a proof in intuitionistic, minimal logic. The conclusion of the resulting proof is the Kolmogorov trnaslation k applied to the original conclusion.
Value parameters
- proof
-
A proof in ND for a sequent Γ :- A
Attributes
- Returns
-
A proof in intuitionistic, minimal ND for the sequent k(Γ) :- k(A)
- Source
- transformation.scala
Applies the Kolmogorov translation k to a formula. This function puts a double negation in front of every subformula, in case this subformula is not negated already.
Applies the Kolmogorov translation k to a formula. This function puts a double negation in front of every subformula, in case this subformula is not negated already.
Value parameters
- formula
-
input formula for the function k
Attributes
- Returns
-
result of applying k to the input formula
- Source
- transformation.scala