nnProver


Formula

Examples

Syntax
phi ::= a,b,c,... | false | true | neg phi | phi and phi | phi or phi | phi -> phi | ea phi | aa phi
  
Common axioms and interesting examples
Monotonicity for ea: ea (a and b) -> ea a and ea b
Necessitation for ea: ea true
Aggregation for ea: ea a and ea b -> ea (a and b)
Interaction between the operators: aa (a -> b) and ea a -> ea b
Axiom D for ea: neg (ea a and ea neg a)
Axiom D for ea and aa: neg (ea a and aa neg a)
Axiom T for ea: ea a -> a
Large model: ea (ea c and d -> aa a or ea b or f) and ea(ea m -> k or ea l or ea n) and aa( ea x and aa y -> ea( ea z and ea w)) -> aa (g or aa h) or ea ea ea ea i or ea(aa o -> ea 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 ^))