p(a).
-p(x) | p(f(x)).
-p(f(f(a))).
ATP will read the file and display (in prolog notation) the 3 clauses together with indices:
(0) :- p(a)
(1) p(x) :- p(f(x))
(2) p(f(f(a))) :-
Enter tX for automated X steps, sX for displaying all clauses containing X or
Please choose two clauses to process:
Now, it is possible either to apply it automatically for X steps using the notation tX or apply resolution/paramodulation on two selected clauses.
Showcase
The application of
CERes to the
Prime proof examples required
the refutation of an unsatisfiable clause set extracted from the proof. This refutation proved to be impossible to attain using several well known compeletely automatic theorem provers (
Otter and
Prover9) already on the case of 2 primes, due to its large size. In order to apply
CERes on the proof, a partial refutation was created by hand[
CERES: An analysis of Fürstenberg's proof of the infinity of primes]. The following
report describes the interactive process of validating and completing this manually obtained refutation using ATP for the case of 3 primes.
Documentation
Please refer to the user manual for more information.
Links
- Proof Tool is a viewer for
LK proofs.
- CERES is a tool for
automated proof analysis.
Contact
If you have any questions, feel free to
contact us: shaolin |@| logic |.| at
