iiProve


Formula

Parameter N =

Examples

Syntax
phi ::= a,b,c,... | false | true | phi and phi | phi or phi | phi -> phi
  
Common axioms
Linearity: (a -> b) or (b -> a)
Bounded depth 2: q or (q -> p or (p -> false))
  Alternatively: ((p -> (((q -> r) -> q) -> q)) -> p) -> p
Smetanich logic: ((q -> false) -> p) -> (((p -> q) -> p) -> p)
Classical logic: p or (p -> false)
Bounded branching 2: (p and q -> r) or (p and r -> q) or (q and r -> p)
K
?(5, p + q) , ?(4, r + t), !(1, p ^ * t ^) 
?(1, q)  && ?(1, p)  && !(1, p ^ * q ^)
?(1, p * q ^) && ?(1, p ^) && !(1, q)
  
K + 4
?(1, p), !(1, !(1, p ^))
?(3, p + q), !(2, !(1, p ^ ))
?(5, p) , ?(4, q), !(2, !(1, p ^ * q ^))
?(3, p ^) , !(2, !(1, p))
  
K + D
?(1,p) , ?(1, p ^)
?(2,?(1, p)) , ?(2, !(1, p ^))
?(1, ?(1, p)) && ?(1, ?(1, p ^))
  
K + T
?(1,p), p ^
  
K + D + 4
?(2, p) && ?(2, ?(1, p ^))
?(3, ?(2, p)) && ?(2, ?(1, p ^))