1. Forum
  2. Usenet
  3. SCI.LOGIC

  • Re: Seventy-Five Problems for Testing Automatic Theorem Provers

    From Julio Di Egidio@21:1/5 to Mild Shock on Mon Dec 9 11:39:49 2024
    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

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mild Shock@21:1/5 to Julio Di Egidio on Mon Dec 9 15:00:01 2024
    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


    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)