1. Forum
  2. Usenet
  3. COMP.LANG.PROLOG

  • Prolog Tribute to Hao Wang

    From Mild Shock@21:1/5 to All on Fri Dec 6 21:15:37 2024
    This code here doesn’t make much sense:

    prove(L --> R):-
    member(A => B,L),
    del(A => B,L,NewL),!,

    One can combine member/2 and del/3 into select/3. select/3
    together with member/2 is part of the Prologue to Prolog:

    **A Prologue for Prolog (working draft)** https://www.complang.tuwien.ac.at/ulrich/iso-prolog/prologue

    So if I further strip away using a two sided sequent,
    I can implement Hoa Wangs implication fagment:

    P1. Initial rule: if λ, ζ are strings of atomic
    formulae, then λ -> ζ is a theorem if some atomic
    formula occurs an both sides of the arrow.

    P5a. Rule —> => If ζ, φ -> λ, ψ, ρ, then ζ -> λ, φ => ψ, ρ P5b. Rule => -> If λ, ψ, ρ -> π and λ, ρ -> π, φ then λ, φ => ψ, ρ -> π

    (Hao Wang. Toward Mechanical Mathematics. IBM
    Journal of Research and Development 4:1 (1960), 15.)

    as follows in 3 lines:

    prove(L) :- select((A->B),L,R), !, prove([-A,B|R]).
    prove(L) :- select(-(A->B),L,R), !, prove([A|R]), prove([-B|R]).
    prove(L) :- select(-A,L,R), member(A,R), !.
    Seems to work, I can prove Peirce Law:

    ?- prove([(((p->q)->p)->p)]).
    true.
    See also:

    **Hao Wang on the formalisation of mathematics**
    Lawrence C. Paulson 26 Jul 2023 https://lawrencecpaulson.github.io/2023/07/26/Wang.html

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mild Shock@21:1/5 to Mild Shock on Sat Dec 7 23:22:06 2024
    Hi,

    But its funny that people still work on UNSAT,
    because its known that SAT is NP complete.

    But don't worry, I sometimes do the same.
    Imogen seems to chocke on SYJ202:

    SYJ202+1.005.imo Provable. Time: 2.129
    SYJ202+1.006.imo Provable. Time: 3.790
    SYJ202+1.007.imo Provable. Time: 16.222
    SYJ202+1.008.imo Provable. Time: 143.802

    I assume its just the same problem linearly growing,
    but the time is exponential or something.

    BTW: Complexity for intuitionistic propositional logic
    is even worse, its PSPACE complete. Here a recent

    attempt featuring intuitRIL and SuperL

    Implementing Intermediate Logics https://iltp.de/ARQNL-2024/download/proceedings_preli/2_ARQNL_2024_paper_8.pdf

    Have Fun!

    Bye

    Mild Shock schrieb:
    This code here doesn’t make much sense:

    prove(L --> R):-
        member(A => B,L),
        del(A => B,L,NewL),!,

    One can combine member/2 and del/3 into select/3. select/3
    together with member/2 is part of the Prologue to Prolog:

    **A Prologue for Prolog (working draft)** https://www.complang.tuwien.ac.at/ulrich/iso-prolog/prologue

    So if I further strip away using a two sided sequent,
    I can implement Hoa Wangs implication fagment:

    P1. Initial rule: if λ, ζ are strings of atomic
    formulae, then λ -> ζ is a theorem if some atomic
    formula occurs an both sides of the arrow.

    P5a. Rule —> =>    If ζ, φ -> λ, ψ, ρ, then ζ -> λ, φ => ψ, ρ P5b. Rule => -> If λ, ψ, ρ -> π and λ, ρ -> π, φ then λ, φ => ψ, ρ -> π

    (Hao Wang. Toward Mechanical Mathematics. IBM
    Journal of Research and Development 4:1 (1960), 15.)

    as follows in 3 lines:

    prove(L) :- select((A->B),L,R), !, prove([-A,B|R]).
    prove(L) :- select(-(A->B),L,R), !, prove([A|R]), prove([-B|R]).
    prove(L) :- select(-A,L,R), member(A,R), !.
    Seems to work, I can prove Peirce Law:

    ?- prove([(((p->q)->p)->p)]).
    true.
    See also:

    **Hao Wang on the formalisation of mathematics**
    Lawrence C. Paulson 26 Jul 2023 https://lawrencecpaulson.github.io/2023/07/26/Wang.html






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