Re: Seventy-Five Problems for Testing Automatic Theorem Provers

Hi,
Test case generator:
?- urquhart(1, X).
X = (x1 <-> x1).
?- urquhart(2, X).
X = (x2 <-> (x1 <-> (x2 <-> x1))).
?- urquhart(3, X).
X = (x3 <-> (x2 <-> (x1 <-> (x3 <-> (x2 <-> x1))))).
Etc..
Using this code:
% urquhart(+Integer, -Expr)
urquhart(N, X) :-
    urquhart(N, x1, Y),
    urquhart(N, (x1<->Y), X).
% urquhart(+Integer, +Expr, -Expr)
urquhart(1, Z, Z) :- !.
urquhart(N, Z, (X<->Y)) :-
    number_codes(N, L),
    atom_codes(X, [0'x|L]),
    M is N-1,
    urquhart(M, Z, Y).
Bye
Julio Di Egidio schrieb:

On 08/12/2024 12:39, Mild Shock wrote:
 

Seventy-Five Problems for Testing Automatic Theorem Provers.
Francis Jeffry Pelletier -June 1986
Journal of Automated Reasoning 2(2):191-216
DOI: 10.1007/BF02432151
https://www.researchgate.net/publication/220531947

 That helps a lot!  Thank you, and Pelletier.
 -Julio