|
 |
 |
 |
 |
 |
Proof Style |
|
|
Sentence Format |
|
|
Lens Magnitude |
|
Lens Width |
|
|
 |
| |
Current URI: http://inference-web.org/proofs/tptp/Problems/LCL/LCL005-1/query.owl#query
Question:
The Whitehead-Russell axiomatisation of the Disjunction/
Negation 2 valued sentential calculus is {AN-1,AN-2,AN-3,
AN-4}. Show that AN-4 can be derived from the Merideth axiom.
Query
cnf(an_4,negated_conjecture,
( ~ is_a_theorem(or(not(or(a,a)),a)) )).
Answers:
Inference Web: [
Home |
Spec |
Browser |
IWBase |
Registrar |
Registry
]
Copyright 2010 Inference Web group.
All Rights Reserved.
