• France is the Fire Nation of Prolog

    From Mostowski Collapse@21:1/5 to All on Wed Jul 21 06:41:43 2021
    After years of enduring abominations such as
    inappropriate use of DCG, pillow web servers and
    Protobufs, leading to a down spiral

    of turning Prolog into a bash scripting language
    with further unholy marriages such as Prolog dicts
    that are always closed or (=>)/2 for SSU,

    there is finally a new book that mentions logic
    programming in connection with Artificial intelligence.
    Disclaimer, didn't read yet, but the context

    looks interesting:

    A Guided Tour of Artificial Intelligence Research - May, 2020
    Logic Programming Pages 83-113 Lallouet, Arnaud (et al.) https://www.springer.com/gp/book/9783030061661

    If you want to find the secret river, join the fire nation:

    Aang Infiltrates a Fire Nation School https://www.youtube.com/watch?v=hu40eO7ox8w

    LoL

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Wed Jul 21 06:48:23 2021
    The opposite evil of turning Prolog into a bash scripting
    language is the motto use CLP(FD) everywhere and the
    library(reif). Didn't fullfil any of its promisses either.

    Mostowski Collapse schrieb am Mittwoch, 21. Juli 2021 um 15:41:44 UTC+2:
    After years of enduring abominations such as
    inappropriate use of DCG, pillow web servers and
    Protobufs, leading to a down spiral

    of turning Prolog into a bash scripting language
    with further unholy marriages such as Prolog dicts
    that are always closed or (=>)/2 for SSU,

    there is finally a new book that mentions logic
    programming in connection with Artificial intelligence.
    Disclaimer, didn't read yet, but the context

    looks interesting:

    A Guided Tour of Artificial Intelligence Research - May, 2020
    Logic Programming Pages 83-113 Lallouet, Arnaud (et al.) https://www.springer.com/gp/book/9783030061661

    If you want to find the secret river, join the fire nation:

    Aang Infiltrates a Fire Nation School https://www.youtube.com/watch?v=hu40eO7ox8w

    LoL

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Thu Jul 22 03:53:48 2021
    One can easily measure the negative impact of spurious choice
    points. Take this naive reverse with spurious choice points:

    rev([], []).
    rev([X|Rest], Ans) :- rev(Rest, L), concatenate(L, [X], Ans).
    rev(_, _) :- fail.

    concatenate([], L, L).
    concatenate([X|L1], L2, [X|L3]) :- concatenate(L1, L2, L3).
    concatenate(_, _, _) :- fail.

    Benchmarking shows, spurious choice points slow
    down nrev by a factor >2x:

    /* without spurious choice points */
    user:nrev in 93 (0 gc) ms

    /* with spurious choice points */
    user:nrev in 234 (0 gc) ms

    So the kind of library(dcg/basics) should be quaranteened. Or put
    into a poison cabinet, and the key then thrown away. Or write tutorial
    that show to write DCG without any spurious choice points.

    Languages that are for example LL(1) do not need any choice point. https://en.wikipedia.org/wiki/LL_grammar

    Mostowski Collapse schrieb am Donnerstag, 22. Juli 2021 um 12:51:46 UTC+2:
    So will the earth benders ever write efficient code? The fire
    nation or the water benders could be ahead of their time,
    but what about the earth benders?

    Here is a DCG code smell:

    % When Type is a variable, backtracks through all the possibilities
    % for a given wire encoding.
    [...]
    prolog_type(Tag, unsigned64) --> protobuf_tag_type(Tag, fixed64). prolog_type(Tag, float) --> protobuf_tag_type(Tag, fixed32).
    prolog_type(Tag, integer32) --> protobuf_tag_type(Tag, fixed32). prolog_type(Tag, unsigned32) --> protobuf_tag_type(Tag, fixed32). prolog_type(Tag, integer) --> protobuf_tag_type(Tag, varint).
    [...]

    Looks nice, but doesn't work. It can lead to spurious choice
    points. This is a widespread inappropriate use of DCG. It is
    declarative and logically correct, good for academic slides.

    But not for production code.
    Mostowski Collapse schrieb am Mittwoch, 21. Juli 2021 um 15:48:24 UTC+2:
    The opposite evil of turning Prolog into a bash scripting
    language is the motto use CLP(FD) everywhere and the
    library(reif). Didn't fullfil any of its promisses either.
    Mostowski Collapse schrieb am Mittwoch, 21. Juli 2021 um 15:41:44 UTC+2:
    After years of enduring abominations such as
    inappropriate use of DCG, pillow web servers and
    Protobufs, leading to a down spiral

    of turning Prolog into a bash scripting language
    with further unholy marriages such as Prolog dicts
    that are always closed or (=>)/2 for SSU,

    there is finally a new book that mentions logic
    programming in connection with Artificial intelligence.
    Disclaimer, didn't read yet, but the context

    looks interesting:

    A Guided Tour of Artificial Intelligence Research - May, 2020
    Logic Programming Pages 83-113 Lallouet, Arnaud (et al.) https://www.springer.com/gp/book/9783030061661

    If you want to find the secret river, join the fire nation:

    Aang Infiltrates a Fire Nation School https://www.youtube.com/watch?v=hu40eO7ox8w

    LoL

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Thu Jul 22 03:51:45 2021
    So will the earth benders ever write efficient code? The fire
    nation or the water benders could be ahead of their time,
    but what about the earth benders?

    Here is a DCG code smell:

    % When Type is a variable, backtracks through all the possibilities
    % for a given wire encoding.
    [...]
    prolog_type(Tag, unsigned64) --> protobuf_tag_type(Tag, fixed64). prolog_type(Tag, float) --> protobuf_tag_type(Tag, fixed32). prolog_type(Tag, integer32) --> protobuf_tag_type(Tag, fixed32). prolog_type(Tag, unsigned32) --> protobuf_tag_type(Tag, fixed32). prolog_type(Tag, integer) --> protobuf_tag_type(Tag, varint).
    [...]

    Looks nice, but doesn't work. It can lead to spurious choice
    points. This is a widespread inappropriate use of DCG. It is
    declarative and logically correct, good for academic slides.

    But not for production code.

    Mostowski Collapse schrieb am Mittwoch, 21. Juli 2021 um 15:48:24 UTC+2:
    The opposite evil of turning Prolog into a bash scripting
    language is the motto use CLP(FD) everywhere and the
    library(reif). Didn't fullfil any of its promisses either.
    Mostowski Collapse schrieb am Mittwoch, 21. Juli 2021 um 15:41:44 UTC+2:
    After years of enduring abominations such as
    inappropriate use of DCG, pillow web servers and
    Protobufs, leading to a down spiral

    of turning Prolog into a bash scripting language
    with further unholy marriages such as Prolog dicts
    that are always closed or (=>)/2 for SSU,

    there is finally a new book that mentions logic
    programming in connection with Artificial intelligence.
    Disclaimer, didn't read yet, but the context

    looks interesting:

    A Guided Tour of Artificial Intelligence Research - May, 2020
    Logic Programming Pages 83-113 Lallouet, Arnaud (et al.) https://www.springer.com/gp/book/9783030061661

    If you want to find the secret river, join the fire nation:

    Aang Infiltrates a Fire Nation School https://www.youtube.com/watch?v=hu40eO7ox8w

    LoL

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Fri Jul 23 03:32:20 2021
    The Kissat SAT solver is a reimplementation of CaDiCaL in C. https://twitter.com/ArminBiere/status/1288132283443142661

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Fri Jul 23 03:46:19 2021
    The rustc linter can be used for SAT solving. https://twitter.com/NieDzejkob/status/1412932919761453058

    LoL

    Mostowski Collapse schrieb am Freitag, 23. Juli 2021 um 12:32:28 UTC+2:
    The Kissat SAT solver is a reimplementation of CaDiCaL in C. https://twitter.com/ArminBiere/status/1288132283443142661

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Wed Jul 28 02:29:33 2021
    The EngineMessage and EngineException combo works
    excellently internally in Java code. But when moving outside
    of Java, into Prolog code, we decided to always convert

    into an error with a backtrace. So inside Prolog code there
    is no more benefit, and calling number_codes/2 inside Prolog
    will not benefit. This is a little annoying for the Dogelog runtime

    which aims at doing more stuff in Prolog itself. So there
    is now a Dogelog runtime proposal, to have a backtrace, and
    maybe even shamelessly adopt catch_with_backtrace/3:

    Use spare wheel for backtrace in throw/1 #86
    https://github.com/jburse/dogelog-moon/issues/86

    Not yet sure. But its not yet clear how this proposal should work
    out, if a catch/3 doesn't catch a ball, and hands it down to catch_with_backtrace/1. How can it add a backtrace after

    the fact? Maybe the rethrow will only have a backtarce
    to catch/3 and not its early history.

    Mostowski Collapse schrieb am Mittwoch, 28. Juli 2021 um 11:19:53 UTC+2:
    SWI-Prolog has an interesting solution to the catch/throw
    problem. It offers two different catch:

    - catch/3: Does not build a backtrace
    - catch_with_backtrace/3: As the name says, builds a backtrace

    We did something else in Jekejeke Prolog. We had two types
    of internal Prolog errors:

    - EngineMessage: Prolog error without backtrace
    - EngineException: Prolog error with backtrace

    This was less motivated by performance considerations, such
    as number_codes/2 exceptions, but rather by the observation that
    some code has access to Engine, and can therefore fetch

    backtrace, and other code does not have an Engine parameter,
    and EngineMessage would be thrown, and the backtrace would be
    fetched later.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Wed Jul 28 02:19:52 2021
    SWI-Prolog has an interesting solution to the catch/throw
    problem. It offers two different catch:

    - catch/3: Does not build a backtrace
    - catch_with_backtrace/3: As the name says, builds a backtrace

    We did something else in Jekejeke Prolog. We had two types
    of internal Prolog errors:

    - EngineMessage: Prolog error without backtrace
    - EngineException: Prolog error with backtrace

    This was less motivated by performance considerations, such
    as number_codes/2 exceptions, but rather by the observation that
    some code has access to Engine, and can therefore fetch

    backtrace, and other code does not have an Engine parameter,
    and EngineMessage would be thrown, and the backtrace would be
    fetched later.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Wed Jul 28 02:42:02 2021
    We would stay in the ISO core standard semantics of catch/throw.
    Like XSB implements it. So despite a new feature with or without
    backtrace, semantics would not deviate from ISO core standard.

    This can be made by letting catch/3 and catch_with_backtrace/3
    not involved in the execution of fetching a backtrace or not,
    this is done further down in the execution, these predicates

    catch/3 and catch_with_backtrace/3 would only set a flag.
    But since they also manage the stack, they can simply color the
    stack, and the top of the stack always tells what was

    requested, i.e. catch/3 or catch_with_backtrace/3. But it is not
    that catch/3 would not anymore build the stack itself, which is
    also some cost. The stack uses some spare wheel of the

    stack datastructure for the colouring. But that datastructure
    needs to be built anyway for other reasons like garbage collection.

    Mostowski Collapse schrieb am Mittwoch, 28. Juli 2021 um 11:29:34 UTC+2:
    The EngineMessage and EngineException combo works
    excellently internally in Java code. But when moving outside
    of Java, into Prolog code, we decided to always convert

    into an error with a backtrace. So inside Prolog code there
    is no more benefit, and calling number_codes/2 inside Prolog
    will not benefit. This is a little annoying for the Dogelog runtime

    which aims at doing more stuff in Prolog itself. So there
    is now a Dogelog runtime proposal, to have a backtrace, and
    maybe even shamelessly adopt catch_with_backtrace/3:

    Use spare wheel for backtrace in throw/1 #86 https://github.com/jburse/dogelog-moon/issues/86

    Not yet sure. But its not yet clear how this proposal should work
    out, if a catch/3 doesn't catch a ball, and hands it down to catch_with_backtrace/1. How can it add a backtrace after

    the fact? Maybe the rethrow will only have a backtarce
    to catch/3 and not its early history.
    Mostowski Collapse schrieb am Mittwoch, 28. Juli 2021 um 11:19:53 UTC+2:
    SWI-Prolog has an interesting solution to the catch/throw
    problem. It offers two different catch:

    - catch/3: Does not build a backtrace
    - catch_with_backtrace/3: As the name says, builds a backtrace

    We did something else in Jekejeke Prolog. We had two types
    of internal Prolog errors:

    - EngineMessage: Prolog error without backtrace
    - EngineException: Prolog error with backtrace

    This was less motivated by performance considerations, such
    as number_codes/2 exceptions, but rather by the observation that
    some code has access to Engine, and can therefore fetch

    backtrace, and other code does not have an Engine parameter,
    and EngineMessage would be thrown, and the backtrace would be
    fetched later.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Tue Oct 26 00:58:18 2021
    Interesting take on a verified SAT solver. They have two proofs.
    One proof shows that the SAT solver is sound and complete
    unconditionally. Such a proof needs to assume natural numbers,

    which are then used to encode literals, clauses, etc.. From such
    a proof one can extract code for an abstract machine that
    has big numbers, that might nevertheless throw a resource

    error when memory is exhaustet. Then they have a second proof
    where they assume a more down to earth encoding of
    literals, clauses, etc.. by assuming stuff is encoded in 64-bit

    or somesuch. In such a proof there is not anymore completeness.
    The SAT solver is already inheritenly incompletely viewed
    on the verification level. Whats the advantage of such an approach?

    Mostowski Collapse schrieb am Dienstag, 26. Oktober 2021 um 09:57:20 UTC+2:
    The SAT solver IsaSAT by Mathias Fleury has won the
    fixed CNF encoding race of the 2021 EDA Challenge. All results.

    IsaSAT is a formally verified SAT solver, using Peter Lammich's
    Isabelle LLVM to produce fast verified code.

    This is the first time a formally verified solver wins a competition
    against unverified solvers.

    http://fmv.jku.at/papers/Fleury-EDA-Challenge-2021.pdf

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Tue Oct 26 00:57:18 2021
    The SAT solver IsaSAT by Mathias Fleury has won the
    fixed CNF encoding race of the 2021 EDA Challenge. All results.

    IsaSAT is a formally verified SAT solver, using Peter Lammich's
    Isabelle LLVM to produce fast verified code.

    This is the first time a formally verified solver wins a competition
    against unverified solvers.

    http://fmv.jku.at/papers/Fleury-EDA-Challenge-2021.pdf

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Tue Oct 26 00:59:30 2021
    Maybe the advantage of such an approach is that exception
    handling can be also verified. If exception handling like a resource
    error is wrongly done, it might lead to false positives or

    negatives. And if the exception handling is not verified
    these false positives or negatives might go unnoticed, when
    they are only imputed in the extracted artefact, and

    not part of the mathematical modelling. On the other hand
    if we have it already verified, we get a more safer implementation.
    But how is this done and how does it related to LLVM?

    Rust has something similar, Rust can be run with bounded
    arithmetic so that x+y does not wrap around but rather
    throws an error when the sum is outside of the type range.

    Such bounded arithmetic could be also modelled logically
    when doing the verification.

    Mostowski Collapse schrieb am Dienstag, 26. Oktober 2021 um 09:58:19 UTC+2:
    Interesting take on a verified SAT solver. They have two proofs.
    One proof shows that the SAT solver is sound and complete
    unconditionally. Such a proof needs to assume natural numbers,

    which are then used to encode literals, clauses, etc.. From such
    a proof one can extract code for an abstract machine that
    has big numbers, that might nevertheless throw a resource

    error when memory is exhaustet. Then they have a second proof
    where they assume a more down to earth encoding of
    literals, clauses, etc.. by assuming stuff is encoded in 64-bit

    or somesuch. In such a proof there is not anymore completeness.
    The SAT solver is already inheritenly incompletely viewed
    on the verification level. Whats the advantage of such an approach?
    Mostowski Collapse schrieb am Dienstag, 26. Oktober 2021 um 09:57:20 UTC+2:
    The SAT solver IsaSAT by Mathias Fleury has won the
    fixed CNF encoding race of the 2021 EDA Challenge. All results.

    IsaSAT is a formally verified SAT solver, using Peter Lammich's
    Isabelle LLVM to produce fast verified code.

    This is the first time a formally verified solver wins a competition against unverified solvers.

    http://fmv.jku.at/papers/Fleury-EDA-Challenge-2021.pdf

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Wed Nov 3 07:47:36 2021
    Now toying around with SWI-Prolog s(CASP). Wonder
    why it has ASP = Answer Set Programming in its name?

    https://swish.swi-prolog.org/p/scasp_constraint_tests.pl

    I am trying this:

    false :- not p, not q.

    p :- p.
    q :- q.

    r :- p.
    r :- q.

    Shouldn’t the query ? r succeed? It gives me false.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Wed Nov 3 07:48:40 2021
    Ok my bad, “not” is not classical negation, even clingo cant
    do it. The clause false :- not p, not q would be logical equivalent
    to p | q :- true if “not” were classical.

    But then I have a disjunctive head. How enter a disjunctive
    head in s(CASP)? In clingo I can do:

    p | q.

    p :- p.
    q :- q.

    r :- p.
    r :- q.

    And as expected it gives me two stable models.

    Answer: 1
    q r
    Answer: 2
    p r

    But SWI-Prolog s(CASP) gives me nothing. Was comparing to:

    https://potassco.org/clingo/run/

    Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:47:38 UTC+1:
    Now toying around with SWI-Prolog s(CASP). Wonder
    why it has ASP = Answer Set Programming in its name?

    https://swish.swi-prolog.org/p/scasp_constraint_tests.pl

    I am trying this:

    false :- not p, not q.

    p :- p.
    q :- q.

    r :- p.
    r :- q.

    Shouldn’t the query ? r succeed? It gives me false.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Thu Nov 4 00:49:24 2021
    So some conclusion was that s(CASP) probably doesn't
    do disjunctive logic programming. The example we had
    was as folllows:

    :- abducible p, q.

    false :- -p, -q.

    r :- p, q.

    https://swish.swi-prolog.org/p/disj_trial3.pl

    From classical logic and also in ordinary ASP, we will
    not find that r occurs in all stable models. On the
    other hand s(CAPS) seems to be able

    to prove both r and not r. LoL

    Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:48:41 UTC+1:
    Ok my bad, “not” is not classical negation, even clingo cant
    do it. The clause false :- not p, not q would be logical equivalent
    to p | q :- true if “not” were classical.

    But then I have a disjunctive head. How enter a disjunctive
    head in s(CASP)? In clingo I can do:

    p | q.
    p :- p.
    q :- q.

    r :- p.
    r :- q.
    And as expected it gives me two stable models.

    Answer: 1
    q r
    Answer: 2
    p r

    But SWI-Prolog s(CASP) gives me nothing. Was comparing to:

    https://potassco.org/clingo/run/
    Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:47:38 UTC+1:
    Now toying around with SWI-Prolog s(CASP). Wonder
    why it has ASP = Answer Set Programming in its name?

    https://swish.swi-prolog.org/p/scasp_constraint_tests.pl

    I am trying this:

    false :- not p, not q.

    p :- p.
    q :- q.

    r :- p.
    r :- q.

    Shouldn’t the query ? r succeed? It gives me false.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Thu Nov 4 00:50:22 2021
    Our own conclusion, that we can prove r and not r,
    was that abduction is involved.

    If P is the s(CASP) program, and A is what was abducted, then
    the s(CASP) query Q is resolved against the program P and the
    the abducted facts A. So that you have:

    P, A |- Q.

    When I asked r, it abducted p,q. When I asked not r, it abducted ~p.
    What was abducted is seen in the s(CASP) model section.
    For example for the abducible fact p, the _p makes ~p.

    Oki Doki.

    Mostowski Collapse schrieb am Donnerstag, 4. November 2021 um 08:49:25 UTC+1:
    So some conclusion was that s(CASP) probably doesn't
    do disjunctive logic programming. The example we had
    was as folllows:

    :- abducible p, q.

    false :- -p, -q.

    r :- p, q.

    https://swish.swi-prolog.org/p/disj_trial3.pl

    From classical logic and also in ordinary ASP, we will
    not find that r occurs in all stable models. On the
    other hand s(CAPS) seems to be able

    to prove both r and not r. LoL
    Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:48:41 UTC+1:
    Ok my bad, “not” is not classical negation, even clingo cant
    do it. The clause false :- not p, not q would be logical equivalent
    to p | q :- true if “not” were classical.

    But then I have a disjunctive head. How enter a disjunctive
    head in s(CASP)? In clingo I can do:

    p | q.
    p :- p.
    q :- q.

    r :- p.
    r :- q.
    And as expected it gives me two stable models.

    Answer: 1
    q r
    Answer: 2
    p r

    But SWI-Prolog s(CASP) gives me nothing. Was comparing to:

    https://potassco.org/clingo/run/
    Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:47:38 UTC+1:
    Now toying around with SWI-Prolog s(CASP). Wonder
    why it has ASP = Answer Set Programming in its name?

    https://swish.swi-prolog.org/p/scasp_constraint_tests.pl

    I am trying this:

    false :- not p, not q.

    p :- p.
    q :- q.

    r :- p.
    r :- q.

    Shouldn’t the query ? r succeed? It gives me false.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sat Nov 6 12:07:32 2021
    There is an interesting relationship to QSAT. Namely
    we can do abduction in QSAT. At least it seems to me.
    First look at deduction and not abduction. Deduction
    would be verification of P |- Q, with P and Q given,

    no abducible A involved. In QSAT we can ask:

    /* SWI-Prolog */
    ?- sat(~(V^ ~(P =< Q))).

    What does this all mean? Well V are the propositional
    variables, and (^)/2 is the QSAT proositional existential
    quantifier, (~)/1 is boolean negation and (=<)/2 is boolean
    implication. So the problem I posed for ASP was simply:

    P: The logic program:
    p v q.
    r <- p & q.

    Q: The query to the logic program:
    ?- r.

    Now with a QSAT solver, such as SWI-Prolog, we see that
    r is not provable, namely we have:

    ?- use_module(library(clpb)).
    true.

    ?- sat(~(P^Q^R^ ~((P+Q)*(R>=P*Q)=<R))).
    false.

    Cool!

    Mostowski Collapse schrieb am Donnerstag, 4. November 2021 um 08:50:23 UTC+1:
    Our own conclusion, that we can prove r and not r,
    was that abduction is involved.

    If P is the s(CASP) program, and A is what was abducted, then
    the s(CASP) query Q is resolved against the program P and the
    the abducted facts A. So that you have:

    P, A |- Q.

    When I asked r, it abducted p,q. When I asked not r, it abducted ~p.
    What was abducted is seen in the s(CASP) model section.
    For example for the abducible fact p, the _p makes ~p.

    Oki Doki.
    Mostowski Collapse schrieb am Donnerstag, 4. November 2021 um 08:49:25 UTC+1:
    So some conclusion was that s(CASP) probably doesn't
    do disjunctive logic programming. The example we had
    was as folllows:

    :- abducible p, q.

    false :- -p, -q.

    r :- p, q.

    https://swish.swi-prolog.org/p/disj_trial3.pl

    From classical logic and also in ordinary ASP, we will
    not find that r occurs in all stable models. On the
    other hand s(CAPS) seems to be able

    to prove both r and not r. LoL
    Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:48:41 UTC+1:
    Ok my bad, “not” is not classical negation, even clingo cant
    do it. The clause false :- not p, not q would be logical equivalent
    to p | q :- true if “not” were classical.

    But then I have a disjunctive head. How enter a disjunctive
    head in s(CASP)? In clingo I can do:

    p | q.
    p :- p.
    q :- q.

    r :- p.
    r :- q.
    And as expected it gives me two stable models.

    Answer: 1
    q r
    Answer: 2
    p r

    But SWI-Prolog s(CASP) gives me nothing. Was comparing to:

    https://potassco.org/clingo/run/
    Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:47:38 UTC+1:
    Now toying around with SWI-Prolog s(CASP). Wonder
    why it has ASP = Answer Set Programming in its name?

    https://swish.swi-prolog.org/p/scasp_constraint_tests.pl

    I am trying this:

    false :- not p, not q.

    p :- p.
    q :- q.

    r :- p.
    r :- q.

    Shouldn’t the query ? r succeed? It gives me false.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sat Nov 6 12:08:26 2021
    Now how do we do abduction. Well we split the propositonal
    variables V into two camps, V1 the abducible ones, and V2
    the normal ones. And then we issue the following question
    towards the QSAT solver:

    /* SWI-Prolog */
    ?- sat(V1 ~(V2^ ~(P =< Q))).

    Lets do this for the example where r wasn't provable from
    deduction alone. We make p and q abducible. Eh voila
    r becomes provable:

    ?- sat(P^Q^ ~(R^ ~((P+Q)*(R>=P*Q)=<R))).
    sat(P=:=P),
    sat(Q=:=Q),
    sat(R=:=R).

    The sat(X=:=X) constraints can be ignored, they just say
    that X is boolean. So this is now basically a true. We can also
    ask ~r, and see that it also becomes provable:

    ?- sat(P^Q^ ~(R^ ~((P+Q)*(R>=P*Q)=< ~R))).
    sat(P=:=P),
    sat(Q=:=Q),
    sat(R=:=R).

    Thats pretty cool!

    Mostowski Collapse schrieb am Samstag, 6. November 2021 um 20:07:33 UTC+1:
    There is an interesting relationship to QSAT. Namely
    we can do abduction in QSAT. At least it seems to me.
    First look at deduction and not abduction. Deduction
    would be verification of P |- Q, with P and Q given,

    no abducible A involved. In QSAT we can ask:

    /* SWI-Prolog */
    ?- sat(~(V^ ~(P =< Q))).

    What does this all mean? Well V are the propositional
    variables, and (^)/2 is the QSAT proositional existential
    quantifier, (~)/1 is boolean negation and (=<)/2 is boolean
    implication. So the problem I posed for ASP was simply:

    P: The logic program:
    p v q.
    r <- p & q.

    Q: The query to the logic program:
    ?- r.

    Now with a QSAT solver, such as SWI-Prolog, we see that
    r is not provable, namely we have:

    ?- use_module(library(clpb)).
    true.

    ?- sat(~(P^Q^R^ ~((P+Q)*(R>=P*Q)=<R))).
    false.

    Cool!
    Mostowski Collapse schrieb am Donnerstag, 4. November 2021 um 08:50:23 UTC+1:
    Our own conclusion, that we can prove r and not r,
    was that abduction is involved.

    If P is the s(CASP) program, and A is what was abducted, then
    the s(CASP) query Q is resolved against the program P and the
    the abducted facts A. So that you have:

    P, A |- Q.

    When I asked r, it abducted p,q. When I asked not r, it abducted ~p.
    What was abducted is seen in the s(CASP) model section.
    For example for the abducible fact p, the _p makes ~p.

    Oki Doki.
    Mostowski Collapse schrieb am Donnerstag, 4. November 2021 um 08:49:25 UTC+1:
    So some conclusion was that s(CASP) probably doesn't
    do disjunctive logic programming. The example we had
    was as folllows:

    :- abducible p, q.

    false :- -p, -q.

    r :- p, q.

    https://swish.swi-prolog.org/p/disj_trial3.pl

    From classical logic and also in ordinary ASP, we will
    not find that r occurs in all stable models. On the
    other hand s(CAPS) seems to be able

    to prove both r and not r. LoL
    Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:48:41 UTC+1:
    Ok my bad, “not” is not classical negation, even clingo cant
    do it. The clause false :- not p, not q would be logical equivalent
    to p | q :- true if “not” were classical.

    But then I have a disjunctive head. How enter a disjunctive
    head in s(CASP)? In clingo I can do:

    p | q.
    p :- p.
    q :- q.

    r :- p.
    r :- q.
    And as expected it gives me two stable models.

    Answer: 1
    q r
    Answer: 2
    p r

    But SWI-Prolog s(CASP) gives me nothing. Was comparing to:

    https://potassco.org/clingo/run/
    Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:47:38 UTC+1:
    Now toying around with SWI-Prolog s(CASP). Wonder
    why it has ASP = Answer Set Programming in its name?

    https://swish.swi-prolog.org/p/scasp_constraint_tests.pl

    I am trying this:

    false :- not p, not q.

    p :- p.
    q :- q.

    r :- p.
    r :- q.

    Shouldn’t the query ? r succeed? It gives me false.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sat Nov 6 12:09:57 2021
    But there are even more tricks in stock with a QSAT
    solver, especially from within Prolog. Works also for
    Jekejeke Prolog not only SWI-Prolog. Namely listing models.
    We can also list the countermodel to our failed prove

    attempt in deduction:

    ?- sat(~((P+Q)*(R>=P*Q)=<R)), labeling([P,Q,R]).
    P = 0, Q = 1, R = 0;
    P = 1, Q = 0, R = 0.

    Where deduction succeeds on the other and, and where
    deduction and abduction is involved, we can list the
    abducibles. Here our first successful deduction and abduction
    test, more information about the abducibles:

    /* Two Models */
    ?- sat(~(R^ ~((P+Q)*(R>=P*Q)=<R))), labeling([P,Q]).
    P = 0, Q = 0;
    P = 1, Q = 1.

    And the second deduction and abduction test:

    /* One Model */
    ?- sat(~(R^ ~((P+Q)*(R>=P*Q)=< ~R))), labeling([P,Q]).
    P = 0, Q = 0.

    The later makes us think about completion. What if
    a Prolog r <- p & q effectively means r <-> p & q. This is
    called closed world assumption. We can also tinker with
    closed world assumption by replacing (>=)/2 by (=:=)/2:

    /* Two Models */
    ?- sat(~(R^ ~((P+Q)*(R=:=P*Q)=<R))), labeling([P,Q]).
    P = 0, Q = 0;
    P = 1, Q = 1.

    /* Three Models */
    ?- sat(~(R^ ~((P+Q)*(R=:=P*Q)=< ~R))), labeling([P,Q]).
    P = 0, Q = 0;
    P = 0, Q = 1;
    P = 1, Q = 0.

    Mostowski Collapse schrieb am Samstag, 6. November 2021 um 20:08:27 UTC+1:
    Now how do we do abduction. Well we split the propositonal
    variables V into two camps, V1 the abducible ones, and V2
    the normal ones. And then we issue the following question
    towards the QSAT solver:

    /* SWI-Prolog */
    ?- sat(V1 ~(V2^ ~(P =< Q))).

    Lets do this for the example where r wasn't provable from
    deduction alone. We make p and q abducible. Eh voila
    r becomes provable:

    ?- sat(P^Q^ ~(R^ ~((P+Q)*(R>=P*Q)=<R))).
    sat(P=:=P),
    sat(Q=:=Q),
    sat(R=:=R).

    The sat(X=:=X) constraints can be ignored, they just say
    that X is boolean. So this is now basically a true. We can also
    ask ~r, and see that it also becomes provable:

    ?- sat(P^Q^ ~(R^ ~((P+Q)*(R>=P*Q)=< ~R))).
    sat(P=:=P),
    sat(Q=:=Q),
    sat(R=:=R).

    Thats pretty cool!
    Mostowski Collapse schrieb am Samstag, 6. November 2021 um 20:07:33 UTC+1:
    There is an interesting relationship to QSAT. Namely
    we can do abduction in QSAT. At least it seems to me.
    First look at deduction and not abduction. Deduction
    would be verification of P |- Q, with P and Q given,

    no abducible A involved. In QSAT we can ask:

    /* SWI-Prolog */
    ?- sat(~(V^ ~(P =< Q))).

    What does this all mean? Well V are the propositional
    variables, and (^)/2 is the QSAT proositional existential
    quantifier, (~)/1 is boolean negation and (=<)/2 is boolean
    implication. So the problem I posed for ASP was simply:

    P: The logic program:
    p v q.
    r <- p & q.

    Q: The query to the logic program:
    ?- r.

    Now with a QSAT solver, such as SWI-Prolog, we see that
    r is not provable, namely we have:

    ?- use_module(library(clpb)).
    true.

    ?- sat(~(P^Q^R^ ~((P+Q)*(R>=P*Q)=<R))).
    false.

    Cool!
    Mostowski Collapse schrieb am Donnerstag, 4. November 2021 um 08:50:23 UTC+1:
    Our own conclusion, that we can prove r and not r,
    was that abduction is involved.

    If P is the s(CASP) program, and A is what was abducted, then
    the s(CASP) query Q is resolved against the program P and the
    the abducted facts A. So that you have:

    P, A |- Q.

    When I asked r, it abducted p,q. When I asked not r, it abducted ~p. What was abducted is seen in the s(CASP) model section.
    For example for the abducible fact p, the _p makes ~p.

    Oki Doki.
    Mostowski Collapse schrieb am Donnerstag, 4. November 2021 um 08:49:25 UTC+1:
    So some conclusion was that s(CASP) probably doesn't
    do disjunctive logic programming. The example we had
    was as folllows:

    :- abducible p, q.

    false :- -p, -q.

    r :- p, q.

    https://swish.swi-prolog.org/p/disj_trial3.pl

    From classical logic and also in ordinary ASP, we will
    not find that r occurs in all stable models. On the
    other hand s(CAPS) seems to be able

    to prove both r and not r. LoL
    Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:48:41 UTC+1:
    Ok my bad, “not” is not classical negation, even clingo cant
    do it. The clause false :- not p, not q would be logical equivalent to p | q :- true if “not” were classical.

    But then I have a disjunctive head. How enter a disjunctive
    head in s(CASP)? In clingo I can do:

    p | q.
    p :- p.
    q :- q.

    r :- p.
    r :- q.
    And as expected it gives me two stable models.

    Answer: 1
    q r
    Answer: 2
    p r

    But SWI-Prolog s(CASP) gives me nothing. Was comparing to:

    https://potassco.org/clingo/run/
    Mostowski Collapse schrieb am Mittwoch, 3. November 2021 um 15:47:38 UTC+1:
    Now toying around with SWI-Prolog s(CASP). Wonder
    why it has ASP = Answer Set Programming in its name?

    https://swish.swi-prolog.org/p/scasp_constraint_tests.pl

    I am trying this:

    false :- not p, not q.

    p :- p.
    q :- q.

    r :- p.
    r :- q.

    Shouldn’t the query ? r succeed? It gives me false.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Wed Nov 10 03:56:12 2021
    Was toying around with proof by cases, two versions
    here of the Yale shooting problem:

    /* s(CAPS) Style */
    https://swish.swi-prolog.org/p/yale_shooting.pl

    /* Negation as Failure Style */ https://swish.swi-prolog.org/p/yale_shooting2.pl

    Had to double check, wasn’t sure anymore about my
    claims. Could be that I am already rusty. Yes if you add
    proof by cases to intuitionistic logic, you get classical logic.
    At last Wikipedia also says so:

    The system of classical logic is obtained by adding any one of the following axioms:

    ϕ ∨ ¬ ϕ (Law of the excluded middle.
    May also be formulated as ( ϕ → χ ) → ( ( ¬ ϕ → χ ) → χ ).)

    https://en.wikipedia.org/wiki/Intuitionistic_logic#Relation_to_classical_logic

    Now (A → (B → C)) is the same as A & B → C, so an alternative
    to the Law of excluded middle (LEM) is indeed proof by cases.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Wed Nov 10 03:58:10 2021
    But s(CAPS) could have some merits over lets say for example
    negation as failure. Most likely s(CAPS) can be approached by
    3-valued logic. There exist approaches to 3-valued logic where a

    predicate p is split into p+ and p-. This would explain the ‘-Name’
    in s(CASP). I made an interesting observation, this 3-valued logic is
    possibly more monotonic than 2-valued logic with negation as failure.

    Which then has impact on embedded implication. We are now talking
    about logic programming and Prolog, and not anymore mathematical
    logic. For example in this example here:

    /* Negation as Failure Style */
    ?- (loaded => dead), dead.
    true ;
    false.

    There is something non-monotonic going on. When I assume p in the
    pressence of negation of failure I effectively assume p+ and retract p-. So
    I am doing two things at once, the retract is a counter factual,

    https://en.wikipedia.org/wiki/Counterfactual_conditional#Logic_and_semantics

    I remove a fact. On the other hand adding embedded implication to s(CASP)
    could lead to more monotonicity. This seen here. We could start with neither
    p+ nor p- present, and this here has two monotonic movements by the

    embedded implication:

    /* s(CAPS) Style */
    ?- (loaded => dead), ('-loaded' => dead).
    true ;
    false.

    Cool!

    Mostowski Collapse schrieb am Mittwoch, 10. November 2021 um 12:56:13 UTC+1:
    Was toying around with proof by cases, two versions
    here of the Yale shooting problem:

    /* s(CAPS) Style */
    https://swish.swi-prolog.org/p/yale_shooting.pl

    /* Negation as Failure Style */ https://swish.swi-prolog.org/p/yale_shooting2.pl

    Had to double check, wasn’t sure anymore about my
    claims. Could be that I am already rusty. Yes if you add
    proof by cases to intuitionistic logic, you get classical logic.
    At last Wikipedia also says so:

    The system of classical logic is obtained by adding any one of the following axioms:

    ϕ ∨ ¬ ϕ (Law of the excluded middle.
    May also be formulated as ( ϕ → χ ) → ( ( ¬ ϕ → χ ) → χ ).)

    https://en.wikipedia.org/wiki/Intuitionistic_logic#Relation_to_classical_logic

    Now (A → (B → C)) is the same as A & B → C, so an alternative
    to the Law of excluded middle (LEM) is indeed proof by cases.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Mon Nov 15 18:54:35 2021
    Strange that the MiniKanren paper doesn’t mention Kunen, Negation in
    logic programming from 1987, where decidability of such constraint
    problems was posited.

    Mostowski Collapse schrieb am Dienstag, 16. November 2021 um 03:46:51 UTC+1:
    I tried this one now with s(CASP):

    p(X,X).

    q(X,Y) :- not p(X,Y).

    ?- ? q(X,Y).

    And it gives me false. I was expecting dif(X,Y) instead.
    Or what is the C in s(CASP)? C stands for constraints, right?

    Edit 16.11.2021:
    The original constructive negation paper (David Chan. 1988.
    Constructive negation based on the completed database. In Proc. of ICLP-88.) would at least require such an answer, since the completion of the fact p(X,X) is:

    p(X,Y) <-> X = Y.

    So when I call not p(X,Y), I basically call not X = Y, and the negation of unification
    would be dif(X,Y) or somesuch. Can be expressed as constraint. The example simple and doesn’t require quantifier elimination.

    MiniKanren has recently tried to handle quantifiers:

    Constructive Negation for MiniKanren http://minikanren.org/workshop/2019/minikanren19-final4.pdf

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Mon Nov 15 18:46:50 2021
    I tried this one now with s(CASP):

    p(X,X).

    q(X,Y) :- not p(X,Y).

    ?- ? q(X,Y).

    And it gives me false. I was expecting dif(X,Y) instead.
    Or what is the C in s(CASP)? C stands for constraints, right?

    Edit 16.11.2021:
    The original constructive negation paper (David Chan. 1988.
    Constructive negation based on the completed database. In Proc. of ICLP-88.) would at least require such an answer, since the completion of the fact p(X,X) is:

    p(X,Y) <-> X = Y.

    So when I call not p(X,Y), I basically call not X = Y, and the negation of unification
    would be dif(X,Y) or somesuch. Can be expressed as constraint. The example simple and doesn’t require quantifier elimination.

    MiniKanren has recently tried to handle quantifiers:

    Constructive Negation for MiniKanren http://minikanren.org/workshop/2019/minikanren19-final4.pdf

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Thu Nov 25 04:25:08 2021
    Looks like Corona had people exploring SWISH.

    Looks like Robert Kowalski is also into the business with
    some s(CASP) variant. In his new paper he also references
    a former project PENG-ASP, but this had one of the classical

    ASP solvers underneath. Maybe there are more test cases
    than only the test case I presented to figure out what s(CASP)
    is doing. But his system emphasis natural language, is baptized

    LE, and the characterization is a little vague. My idea that it does
    also do abduction might be totally wrong. It could be even the
    case that the example they show “query one with scenario two”,

    is in fact embedded implication, “scenario two” => “query one”:

    But, different from ACE and PENG, which are syntactic sugar
    for first-order logic, LE is syntactic sugar for a variant of pure
    Prolog, which is a non-monotonic, meta (or higher-order) logic.
    The relationship of LE to this variant of Prolog is similar to the
    relationship of PENG-ASP to the LP language ASP.
    Logical English for Legal Applications
    November 2021 - Robert Kowalski, Miguel Calejo and Jacinto Dávila
    https://www.researchgate.net/publication/356287669

    Pure Prolog and non-monotonic is a little in contradiction? :astonished:
    Yes and No. The Clark Completion is non-monotonic.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sun Nov 28 07:29:15 2021
    This is also an interesting article, mentioning a new
    trend such as "Multiparadigm languages":

    Where Programming, Ops, AI, and the Cloud are Headed in 2021 https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/

    We just observed that Python 3.10 introduced a new
    pattern matching construct. Now there is a proposal
    for Java JDK 17 followup for some pattern matching
    like switch statement. I guess there is an unspoken law:

    "Every programming language over the long
    run will evolve into some Prolog variant"

    Well this is too harsh, maybe this pattern matching only
    mimicks Haskell single sided unification and not Prolog
    unification. But what if people get fed up
    with single sided unification?

    LoL

    Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1:
    This shows me that functional programming is on the decline:

    Google Trends: Logic vs Functional Programming - From 2004 to 2021 https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming

    I wonder whether this will have an impact on proof assistants.
    Some of them have clearly a functional programming inclining.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Sun Nov 28 07:22:26 2021
    This shows me that functional programming is on the decline:

    Google Trends: Logic vs Functional Programming - From 2004 to 2021 https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming

    I wonder whether this will have an impact on proof assistants.
    Some of them have clearly a functional programming inclining.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sun Nov 28 11:31:10 2021
    Maybe the assumption that programming language further
    evolve is wrong, they could also devolve to assembler again?

    Awaken In 2505, Humans Devolve
    https://www.youtube.com/watch?v=mnLxc954ipo

    At least this would truely help to have full control of
    the performance and memory allocation of your code.

    LMAO!

    Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:29:16 UTC+1:
    This is also an interesting article, mentioning a new
    trend such as "Multiparadigm languages":

    Where Programming, Ops, AI, and the Cloud are Headed in 2021 https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/

    We just observed that Python 3.10 introduced a new
    pattern matching construct. Now there is a proposal
    for Java JDK 17 followup for some pattern matching
    like switch statement. I guess there is an unspoken law:

    "Every programming language over the long
    run will evolve into some Prolog variant"

    Well this is too harsh, maybe this pattern matching only
    mimicks Haskell single sided unification and not Prolog
    unification. But what if people get fed up
    with single sided unification?

    LoL
    Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1:
    This shows me that functional programming is on the decline:

    Google Trends: Logic vs Functional Programming - From 2004 to 2021 https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming

    I wonder whether this will have an impact on proof assistants.
    Some of them have clearly a functional programming inclining.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sun Nov 28 15:24:14 2021
    Anyway, these bitrot exchanges are mushrooming,
    what about this one, would it be helpful?

    https://cs.stackexchange.com/

    Mostowski Collapse schrieb am Montag, 29. November 2021 um 00:20:32 UTC+1:
    There was a proposal: https://area51.stackexchange.com/proposals/29144/beginner-theoretical-computer-science
    But it now says:
    This proposal has been deleted

    Now if you want to join cstheory.stackexchange.com it
    says Anybody can ask a question Anybody can answer
    The best answers are voted up and rise to the top

    But if you do that, they slap their policy into your face:
    It allows only questions that "can be discussed between
    two professors or between two graduate students working
    on Ph.D.'s, but not usually between a professor and a
    typical undergraduate student". https://meta.stackexchange.com/questions/79351/should-research-level-only-sites-be-allowed

    I am not lying when I say even Andrej Bauer did
    that. But how do you want to launch a proof assistants
    site, I assume for everybody? if you cannot divert
    cs theory questions to another stackexchange?

    proof assistants are full of cs theory stuff.
    Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 20:31:11 UTC+1:
    Maybe the assumption that programming language further
    evolve is wrong, they could also devolve to assembler again?

    Awaken In 2505, Humans Devolve
    https://www.youtube.com/watch?v=mnLxc954ipo

    At least this would truely help to have full control of
    the performance and memory allocation of your code.

    LMAO!
    Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:29:16 UTC+1:
    This is also an interesting article, mentioning a new
    trend such as "Multiparadigm languages":

    Where Programming, Ops, AI, and the Cloud are Headed in 2021 https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/

    We just observed that Python 3.10 introduced a new
    pattern matching construct. Now there is a proposal
    for Java JDK 17 followup for some pattern matching
    like switch statement. I guess there is an unspoken law:

    "Every programming language over the long
    run will evolve into some Prolog variant"

    Well this is too harsh, maybe this pattern matching only
    mimicks Haskell single sided unification and not Prolog
    unification. But what if people get fed up
    with single sided unification?

    LoL
    Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1:
    This shows me that functional programming is on the decline:

    Google Trends: Logic vs Functional Programming - From 2004 to 2021 https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming

    I wonder whether this will have an impact on proof assistants.
    Some of them have clearly a functional programming inclining.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sun Nov 28 15:20:30 2021
    There was a proposal: https://area51.stackexchange.com/proposals/29144/beginner-theoretical-computer-science
    But it now says:
    This proposal has been deleted

    Now if you want to join cstheory.stackexchange.com it
    says Anybody can ask a question Anybody can answer
    The best answers are voted up and rise to the top

    But if you do that, they slap their policy into your face:
    It allows only questions that "can be discussed between
    two professors or between two graduate students working
    on Ph.D.'s, but not usually between a professor and a
    typical undergraduate student". https://meta.stackexchange.com/questions/79351/should-research-level-only-sites-be-allowed

    I am not lying when I say even Andrej Bauer did
    that. But how do you want to launch a proof assistants
    site, I assume for everybody? if you cannot divert
    cs theory questions to another stackexchange?

    proof assistants are full of cs theory stuff.

    Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 20:31:11 UTC+1:
    Maybe the assumption that programming language further
    evolve is wrong, they could also devolve to assembler again?

    Awaken In 2505, Humans Devolve
    https://www.youtube.com/watch?v=mnLxc954ipo

    At least this would truely help to have full control of
    the performance and memory allocation of your code.

    LMAO!
    Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:29:16 UTC+1:
    This is also an interesting article, mentioning a new
    trend such as "Multiparadigm languages":

    Where Programming, Ops, AI, and the Cloud are Headed in 2021 https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/

    We just observed that Python 3.10 introduced a new
    pattern matching construct. Now there is a proposal
    for Java JDK 17 followup for some pattern matching
    like switch statement. I guess there is an unspoken law:

    "Every programming language over the long
    run will evolve into some Prolog variant"

    Well this is too harsh, maybe this pattern matching only
    mimicks Haskell single sided unification and not Prolog
    unification. But what if people get fed up
    with single sided unification?

    LoL
    Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1:
    This shows me that functional programming is on the decline:

    Google Trends: Logic vs Functional Programming - From 2004 to 2021 https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming

    I wonder whether this will have an impact on proof assistants.
    Some of them have clearly a functional programming inclining.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Tue Nov 30 06:07:26 2021
    The devolution could be also a form of evolution. I recently saw
    a book about ARM assembly which had a garbage collection
    section. In 2018 ARM started supporting pointer tagging.

    See also:

    ARM Memory Tagging Extension
    Kosty Serbryany - 2019 https://www.usenix.org/system/files/login/articles/login_summer19_03_serebryany.pdf

    C–: a portable assembly language that supports garbage collection
    Simon Peyton Jones - 1999
    https://www.cs.tufts.edu/~nr/pubs/c–gc.pdf

    Basically what was once conceived as a Java Chip seems to
    happen right now. You can also view it as LISP on a Chip I guess,
    remove the object oriented obsession, and focus on safety.

    Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 20:31:11 UTC+1:
    Maybe the assumption that programming language further
    evolve is wrong, they could also devolve to assembler again?

    Awaken In 2505, Humans Devolve
    https://www.youtube.com/watch?v=mnLxc954ipo

    At least this would truely help to have full control of
    the performance and memory allocation of your code.

    LMAO!
    Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:29:16 UTC+1:
    This is also an interesting article, mentioning a new
    trend such as "Multiparadigm languages":

    Where Programming, Ops, AI, and the Cloud are Headed in 2021 https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/

    We just observed that Python 3.10 introduced a new
    pattern matching construct. Now there is a proposal
    for Java JDK 17 followup for some pattern matching
    like switch statement. I guess there is an unspoken law:

    "Every programming language over the long
    run will evolve into some Prolog variant"

    Well this is too harsh, maybe this pattern matching only
    mimicks Haskell single sided unification and not Prolog
    unification. But what if people get fed up
    with single sided unification?

    LoL
    Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1:
    This shows me that functional programming is on the decline:

    Google Trends: Logic vs Functional Programming - From 2004 to 2021 https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming

    I wonder whether this will have an impact on proof assistants.
    Some of them have clearly a functional programming inclining.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Wed Dec 15 04:42:50 2021
    What about this riddle, doing it in Prolog, s(CASP) or LK?
    (LK as per the Phil Zucker page might not do it,
    would need a FOL or so extension I guess)

    An impossible asylum - Avigad et al. 2021
    “In 1982, Raymond Smullyan published an article, “The Asylum of
    Doctor Tarr and Professor Fether,” that consists of a series of
    puzzles. These were later reprinted in the anthology, “The Lady
    or The Tiger? and Other Logic Puzzles.” The last puzzle, which
    describes the asylum alluded to in the title, was designed to be
    especially difficult. With the help of automated reasoning, we
    show that the puzzle’s hypotheses are, in fact, inconsistent,
    which is to say, no such asylum can possibly exist.” https://arxiv.org/abs/2112.02142

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Fri Dec 17 08:59:54 2021
    No Son of BirdBrain III yet in sight?
    I tried https://www.umsu.de/trees/ on this here, to find a model of:

    E * x = x. % left identity
    x’ * x = E. % left inverse
    (x * y) * z = x * (y * z). % associativity
    A * B != B * A. % A and B do not commute

    But its horribly choking.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Tue Dec 28 10:26:20 2021
    Interesting call:

    "For example, have a look at the Coq standard libarary or
    the user contributions, these are formalizations of
    mathematics in type theory. And this stuff is written mostly
    by computer scientists. If mathematicians moved onto
    the proof-assistant bandwagon, there would be much more." https://mathoverflow.net/a/133599

    Maybe they would join the bandwagon if there were
    less typos? Whats a "libarary"? Is it library? Or libarray?

    LoL

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Wed Dec 29 14:46:27 2021
    Small bug in the LK code:

    There is a nice theorem prover for propositional logic with LK implemented in Prolog here:
    https://www.philipzucker.com/javascript-automated-proving/

    Its not complete for FOL matrices, try this:

    prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
    Failed To Prove.

    Now remove the cut in the axiom rule:

    prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
    X = s

    Mostowski Collapse schrieb am Dienstag, 28. Dezember 2021 um 19:26:21 UTC+1:
    Interesting call:

    "For example, have a look at the Coq standard libarary or
    the user contributions, these are formalizations of
    mathematics in type theory. And this stuff is written mostly
    by computer scientists. If mathematicians moved onto
    the proof-assistant bandwagon, there would be much more." https://mathoverflow.net/a/133599

    Maybe they would join the bandwagon if there were
    less typos? Whats a "libarary"? Is it library? Or libarray?

    LoL

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Thu Dec 30 01:06:48 2021
    Oh, this is very nice!

    ∃x∃y(Pyy → Pxf(x)) is invalid. https://www.umsu.de/trees/#~7x~7y%28Pyy~5Pxf%28x%29%29

    Countermodel:
    Domain: { 0, 1 }
    f: { (0,1), (1,0) }
    P: { (0,0), (1,1) }

    Mostowski Collapse schrieb am Donnerstag, 30. Dezember 2021 um 09:56:23 UTC+1:
    To handle FOL matrices, unify_with_occurs_check/2 might
    also come into play. Whats a short example and short
    explanation about things that can go wrong?

    Mostowski Collapse schrieb:
    Small bug in the LK code:

    There is a nice theorem prover for propositional logic with LK implemented in Prolog here:
    https://www.philipzucker.com/javascript-automated-proving/

    Its not complete for FOL matrices, try this:

    prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
    Failed To Prove.

    Now remove the cut in the axiom rule:

    prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
    X = s

    Mostowski Collapse schrieb am Dienstag, 28. Dezember 2021 um 19:26:21 UTC+1:
    Interesting call:

    "For example, have a look at the Coq standard libarary or
    the user contributions, these are formalizations of
    mathematics in type theory. And this stuff is written mostly
    by computer scientists. If mathematicians moved onto
    the proof-assistant bandwagon, there would be much more."
    https://mathoverflow.net/a/133599

    Maybe they would join the bandwagon if there were
    less typos? Whats a "libarary"? Is it library? Or libarray?

    LoL

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Thu Dec 30 09:56:21 2021
    To handle FOL matrices, unify_with_occurs_check/2 might
    also come into play. Whats a short example and short
    explanation about things that can go wrong?

    Mostowski Collapse schrieb:
    Small bug in the LK code:

    There is a nice theorem prover for propositional logic with LK implemented in Prolog here:
    https://www.philipzucker.com/javascript-automated-proving/

    Its not complete for FOL matrices, try this:

    prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
    Failed To Prove.

    Now remove the cut in the axiom rule:

    prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
    X = s

    Mostowski Collapse schrieb am Dienstag, 28. Dezember 2021 um 19:26:21 UTC+1:
    Interesting call:

    "For example, have a look at the Coq standard libarary or
    the user contributions, these are formalizations of
    mathematics in type theory. And this stuff is written mostly
    by computer scientists. If mathematicians moved onto
    the proof-assistant bandwagon, there would be much more."
    https://mathoverflow.net/a/133599

    Maybe they would join the bandwagon if there were
    less typos? Whats a "libarary"? Is it library? Or libarray?

    LoL

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Julio Di Egidio@21:1/5 to burs...@gmail.com on Thu Dec 30 02:48:08 2021
    On Thursday, 30 December 2021 at 10:06:49 UTC+1, burs...@gmail.com wrote:

    Oh, this is very nice!

    There is nothing nice about a fucking retard and piece of spamming
    shit polluting all public ponds, you shameless retarded piece of shit.

    But all I'd still want to know is who's the criminal nazi cunts who pay your bills...

    *Plonk*

    Julio

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Julio Di Egidio on Thu Dec 30 04:38:20 2021
    LoL, are you feeling tense Culio?

    Julio Di Egidio <julio@diegidio.name> schrieb am Donnerstag, 30. Dezember 2021 um 11:48:09 UTC+1:
    On Thursday, 30 December 2021 at 10:06:49 UTC+1, burs...@gmail.com wrote:

    Oh, this is very nice!
    There is nothing nice about a fucking retard and piece of spamming
    shit polluting all public ponds, you shameless retarded piece of shit.

    But all I'd still want to know is who's the criminal nazi cunts who pay your bills...

    *Plonk*

    Julio

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Fri Dec 31 01:11:36 2021
    Lean TAP can be fun. Spent the whole day to
    render MathJax. Then was annoyed by MathJax,
    how do you put this thingy into an email?

    So here is barber paradox in list form with Unicode:

    1. s(a,a) ⊢ s(a,a) (ax)
    2. s(a,a) ⊢ ∃zs(z,z) (R∃)
    3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
    4. s(a,a) ⊢ s(a,a) (ax)
    5. s(a,a) ⊢ ∃zs(z,z) (R∃)
    6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
    7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
    8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
    9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)

    http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sat Jan 1 03:30:23 2022
    So how was it done? First one needs to reduce proof noise:

    Dogelog Player removes proof noise https://twitter.com/dogelogch/status/1477236879795830785

    Dogelog Player removes proof noise
    https://www.facebook.com/groups/dogelog

    Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1:
    Lean TAP can be fun. Spent the whole day to
    render MathJax. Then was annoyed by MathJax,
    how do you put this thingy into an email?

    So here is barber paradox in list form with Unicode:

    1. s(a,a) ⊢ s(a,a) (ax)
    2. s(a,a) ⊢ ∃zs(z,z) (R∃)
    3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
    4. s(a,a) ⊢ s(a,a) (ax)
    5. s(a,a) ⊢ ∃zs(z,z) (R∃)
    6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
    7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
    8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
    9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)

    http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sun Jan 2 15:28:59 2022
    Oki Doki, full first order logic can be also rendered now:

    Leibniz’s Dream in Dogelog Player https://twitter.com/dogelogch/status/1477779371628933121

    Leibniz’s Dream in Dogelog Player
    https://www.facebook.com/groups/dogelog

    Mostowski Collapse schrieb am Samstag, 1. Januar 2022 um 12:30:25 UTC+1:
    So how was it done? First one needs to reduce proof noise:

    Dogelog Player removes proof noise https://twitter.com/dogelogch/status/1477236879795830785

    Dogelog Player removes proof noise
    https://www.facebook.com/groups/dogelog
    Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1:
    Lean TAP can be fun. Spent the whole day to
    render MathJax. Then was annoyed by MathJax,
    how do you put this thingy into an email?

    So here is barber paradox in list form with Unicode:

    1. s(a,a) ⊢ s(a,a) (ax)
    2. s(a,a) ⊢ ∃zs(z,z) (R∃)
    3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
    4. s(a,a) ⊢ s(a,a) (ax)
    5. s(a,a) ⊢ ∃zs(z,z) (R∃)
    6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
    7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
    8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
    9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)

    http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Tue Jan 4 02:49:52 2022
    I am afraid, I didn't post the full Barber Paradox. I only posted
    what was found in Jens Ottens ex_barber.pl. Now a regret not
    providing (<=>)/2 in my leanseq_v5.pl fork. The two sided barber
    paradox cannot so concisely be formulate without (<=>)/2.

    What would be fun is not only XOR-SAT but also XOR-FOL.
    The Jens Otten provers can solve FOL problems among which
    we also find FOL problems in prenex normal form Q1x1…QnxnM

    where Q1,…,Qn are the alternating quantifier blocks and M is
    the FOL matrix. Quantifiers are handled in Jens Otten provers:

    Qj=∀: is handled by a Skolem function.
    Qj=∃: is handled by fresh variable and contraction.

    Besides that all the 3 provers he presents, leanseq_v5.pl,
    leantap_pure.pl and leancop_pure.pl do the same with the
    FOL matrix M, they put it into conjunctive normal form (CNF),
    and try to solve it via unification. Lets take the Barber Paradox

    and see how the CNF looks like. The Barber Paradox with (<=>)/2:

    ¬∃x∀y(¬s(y,y) <=> s(x,y))

    The Barber Paradox in prenex with CNF:

    ∀x∃y((¬s(y,y) | s(x,y)) & (s(y,y) | ¬s(x,y))

    When the above is solved unification wise the same thing
    happens twice for both conjuncts. But since the XOR-SAT
    rewriting prototype has simp(A=A, 1) does this mean we could
    solve XOR-FOL differently and for example have a FOL matrix

    format where we solve P<=>Q by directly trying to unify P and Q?

    Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 00:29:00 UTC+1:
    Oki Doki, full first order logic can be also rendered now:

    Leibniz’s Dream in Dogelog Player https://twitter.com/dogelogch/status/1477779371628933121

    Leibniz’s Dream in Dogelog Player
    https://www.facebook.com/groups/dogelog
    Mostowski Collapse schrieb am Samstag, 1. Januar 2022 um 12:30:25 UTC+1:
    So how was it done? First one needs to reduce proof noise:

    Dogelog Player removes proof noise https://twitter.com/dogelogch/status/1477236879795830785

    Dogelog Player removes proof noise
    https://www.facebook.com/groups/dogelog
    Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1:
    Lean TAP can be fun. Spent the whole day to
    render MathJax. Then was annoyed by MathJax,
    how do you put this thingy into an email?

    So here is barber paradox in list form with Unicode:

    1. s(a,a) ⊢ s(a,a) (ax)
    2. s(a,a) ⊢ ∃zs(z,z) (R∃)
    3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
    4. s(a,a) ⊢ s(a,a) (ax)
    5. s(a,a) ⊢ ∃zs(z,z) (R∃)
    6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
    7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
    8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
    9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)

    http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Tue Jan 4 03:28:21 2022
    Nice! Now the example runs also from within Python. Even
    on ordinary CMD on Windows 10. Just use for example this
    font *NSimSum*, select it in the console properties.

    See also:

    Unicode Proof Listing in Dogelog Player https://twitter.com/dogelogch/status/1478315286491287553

    Unicode Proof Listing in Dogelog Player
    https://www.facebook.com/groups/dogelog

    But I have to simplify the Python Dogelog Player console.
    Now the Python Dogelog Player console is a tutorial example,
    but dogelog.py should do it by default.

    Please be patient.

    Mostowski Collapse schrieb am Dienstag, 4. Januar 2022 um 11:49:53 UTC+1:
    I am afraid, I didn't post the full Barber Paradox. I only posted
    what was found in Jens Ottens ex_barber.pl. Now a regret not
    providing (<=>)/2 in my leanseq_v5.pl fork. The two sided barber
    paradox cannot so concisely be formulate without (<=>)/2.

    What would be fun is not only XOR-SAT but also XOR-FOL.
    The Jens Otten provers can solve FOL problems among which
    we also find FOL problems in prenex normal form Q1x1…QnxnM

    where Q1,…,Qn are the alternating quantifier blocks and M is
    the FOL matrix. Quantifiers are handled in Jens Otten provers:

    Qj=∀: is handled by a Skolem function.
    Qj=∃: is handled by fresh variable and contraction.

    Besides that all the 3 provers he presents, leanseq_v5.pl,
    leantap_pure.pl and leancop_pure.pl do the same with the
    FOL matrix M, they put it into conjunctive normal form (CNF),
    and try to solve it via unification. Lets take the Barber Paradox

    and see how the CNF looks like. The Barber Paradox with (<=>)/2:

    ¬∃x∀y(¬s(y,y) <=> s(x,y))

    The Barber Paradox in prenex with CNF:

    ∀x∃y((¬s(y,y) | s(x,y)) & (s(y,y) | ¬s(x,y))

    When the above is solved unification wise the same thing
    happens twice for both conjuncts. But since the XOR-SAT
    rewriting prototype has simp(A=A, 1) does this mean we could
    solve XOR-FOL differently and for example have a FOL matrix

    format where we solve P<=>Q by directly trying to unify P and Q?
    Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 00:29:00 UTC+1:
    Oki Doki, full first order logic can be also rendered now:

    Leibniz’s Dream in Dogelog Player https://twitter.com/dogelogch/status/1477779371628933121

    Leibniz’s Dream in Dogelog Player https://www.facebook.com/groups/dogelog
    Mostowski Collapse schrieb am Samstag, 1. Januar 2022 um 12:30:25 UTC+1:
    So how was it done? First one needs to reduce proof noise:

    Dogelog Player removes proof noise https://twitter.com/dogelogch/status/1477236879795830785

    Dogelog Player removes proof noise https://www.facebook.com/groups/dogelog
    Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1:
    Lean TAP can be fun. Spent the whole day to
    render MathJax. Then was annoyed by MathJax,
    how do you put this thingy into an email?

    So here is barber paradox in list form with Unicode:

    1. s(a,a) ⊢ s(a,a) (ax)
    2. s(a,a) ⊢ ∃zs(z,z) (R∃)
    3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
    4. s(a,a) ⊢ s(a,a) (ax)
    5. s(a,a) ⊢ ∃zs(z,z) (R∃)
    6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
    7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
    8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
    9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)

    http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Tue Jan 4 03:46:28 2022
    Holy cow, the monke army is in full bloom, now
    #Python trending on Twitter!!! So “Digital Twin”
    is the new name for software agent?

    https://towardsdatascience.com/digital-twin-with-python-a-hands-on-example-2a3036124b61

    Mostowski Collapse schrieb am Dienstag, 4. Januar 2022 um 12:28:22 UTC+1:
    Nice! Now the example runs also from within Python. Even
    on ordinary CMD on Windows 10. Just use for example this
    font *NSimSum*, select it in the console properties.

    See also:

    Unicode Proof Listing in Dogelog Player https://twitter.com/dogelogch/status/1478315286491287553

    Unicode Proof Listing in Dogelog Player https://www.facebook.com/groups/dogelog

    But I have to simplify the Python Dogelog Player console.
    Now the Python Dogelog Player console is a tutorial example,
    but dogelog.py should do it by default.

    Please be patient.
    Mostowski Collapse schrieb am Dienstag, 4. Januar 2022 um 11:49:53 UTC+1:
    I am afraid, I didn't post the full Barber Paradox. I only posted
    what was found in Jens Ottens ex_barber.pl. Now a regret not
    providing (<=>)/2 in my leanseq_v5.pl fork. The two sided barber
    paradox cannot so concisely be formulate without (<=>)/2.

    What would be fun is not only XOR-SAT but also XOR-FOL.
    The Jens Otten provers can solve FOL problems among which
    we also find FOL problems in prenex normal form Q1x1…QnxnM

    where Q1,…,Qn are the alternating quantifier blocks and M is
    the FOL matrix. Quantifiers are handled in Jens Otten provers:

    Qj=∀: is handled by a Skolem function.
    Qj=∃: is handled by fresh variable and contraction.

    Besides that all the 3 provers he presents, leanseq_v5.pl,
    leantap_pure.pl and leancop_pure.pl do the same with the
    FOL matrix M, they put it into conjunctive normal form (CNF),
    and try to solve it via unification. Lets take the Barber Paradox

    and see how the CNF looks like. The Barber Paradox with (<=>)/2:

    ¬∃x∀y(¬s(y,y) <=> s(x,y))

    The Barber Paradox in prenex with CNF:

    ∀x∃y((¬s(y,y) | s(x,y)) & (s(y,y) | ¬s(x,y))

    When the above is solved unification wise the same thing
    happens twice for both conjuncts. But since the XOR-SAT
    rewriting prototype has simp(A=A, 1) does this mean we could
    solve XOR-FOL differently and for example have a FOL matrix

    format where we solve P<=>Q by directly trying to unify P and Q?
    Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 00:29:00 UTC+1:
    Oki Doki, full first order logic can be also rendered now:

    Leibniz’s Dream in Dogelog Player https://twitter.com/dogelogch/status/1477779371628933121

    Leibniz’s Dream in Dogelog Player https://www.facebook.com/groups/dogelog
    Mostowski Collapse schrieb am Samstag, 1. Januar 2022 um 12:30:25 UTC+1:
    So how was it done? First one needs to reduce proof noise:

    Dogelog Player removes proof noise https://twitter.com/dogelogch/status/1477236879795830785

    Dogelog Player removes proof noise https://www.facebook.com/groups/dogelog
    Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1:
    Lean TAP can be fun. Spent the whole day to
    render MathJax. Then was annoyed by MathJax,
    how do you put this thingy into an email?

    So here is barber paradox in list form with Unicode:

    1. s(a,a) ⊢ s(a,a) (ax)
    2. s(a,a) ⊢ ∃zs(z,z) (R∃)
    3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬)
    4. s(a,a) ⊢ s(a,a) (ax)
    5. s(a,a) ⊢ ∃zs(z,z) (R∃)
    6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3)
    7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀)
    8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃)
    9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒)

    http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Sat Jan 8 05:06:41 2022
    Now having more fun with Jens Ottens Lean Prover. This
    is a nice little example, where 1 contraction doesn’t work,
    but 2 contractions work:

    ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 1), !.
    fail.
    ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 2), !.
    true.

    See also:

    Maslovs Method in Dogelog Player https://twitter.com/dogelogch/status/1479792480908414979

    Maslovs Method in Dogelog Player
    https://www.facebook.com/groups/dogelog

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sat Jan 8 07:57:44 2022
    The problem with the French logician is, that he does not
    get through the thicket of classical logic into the Maslovs method.
    He only shows a translation for intuitionstic logic in the following form:

    (∃xA)* := ∃x !A
    https://girard.perso.math.cnrs.fr/Synsem.pdf

    Given his other definitions for other connectives and quantifiers
    it might work. In his “Table 2: Classical connectives : definition in
    terms of linear logic” he then repeats this translation.

    I think his translation works since he has exponentation
    elsewhere outside of the quantifier. But the Maslov method shows
    that the outside exponentation in classical connectives is

    superflous, and that we can put the exponentiation in front
    of a certain quantifier.

    Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 14:06:42 UTC+1:
    Now having more fun with Jens Ottens Lean Prover. This
    is a nice little example, where 1 contraction doesn’t work,
    but 2 contractions work:

    ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 1), !.
    fail.
    ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 2), !.
    true.

    See also:

    Maslovs Method in Dogelog Player https://twitter.com/dogelogch/status/1479792480908414979

    Maslovs Method in Dogelog Player
    https://www.facebook.com/groups/dogelog

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sun Jan 9 00:58:55 2022
    Somehow being less obsessed with Curry-Howard isomorphism
    pays off. Everything is Prolog terms, and maybe some of its
    arguments are integers. So what? Proofs are anyway finitistic.

    I wonder what happens if I would do some meta logic and
    strip myself from lambda calculus translations, going without
    logical frameworks or higher-order abstract syntax.

    Making also ideas of λ-Prolog obsolete. Hm..

    Mostowski Collapse schrieb am Sonntag, 9. Januar 2022 um 09:30:13 UTC+1:
    One more iteration of our prover:

    Proof systems that are based on the Howard-Curry isomorphism
    and that extract proof terms in the lambda calculus are familiar
    to node dropping. Lambda calculus expressions have a notion
    of variable occurence.

    /* Eta Reduction */
    λx(Mx) ~~> M for x ∉ M

    Variable occurence can then be used similarly to has_usage/2
    to shorten proof terms in the form of lambda expressions. A
    prominent reduction rule is seen in the above that goes by
    the name eta reduction.

    Our provers do extract terms where we store integer sequent
    indexes of used formulas. For the newest variant we generalized
    the terms to alfa, beta, gamma and delta, but we currently do
    not use a generic binder format.

    See also:

    Node Dropping for Maslovs Method https://twitter.com/dogelogch/status/1480091985222451201

    Node Dropping for Maslovs Method
    https://www.facebook.com/groups/dogelog
    Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 16:57:45 UTC+1:
    The problem with the French logician is, that he does not
    get through the thicket of classical logic into the Maslovs method.
    He only shows a translation for intuitionstic logic in the following form:

    (∃xA)* := ∃x !A
    https://girard.perso.math.cnrs.fr/Synsem.pdf

    Given his other definitions for other connectives and quantifiers
    it might work. In his “Table 2: Classical connectives : definition in terms of linear logic” he then repeats this translation.

    I think his translation works since he has exponentation
    elsewhere outside of the quantifier. But the Maslov method shows
    that the outside exponentation in classical connectives is

    superflous, and that we can put the exponentiation in front
    of a certain quantifier.
    Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 14:06:42 UTC+1:
    Now having more fun with Jens Ottens Lean Prover. This
    is a nice little example, where 1 contraction doesn’t work,
    but 2 contractions work:

    ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 1), !.
    fail.
    ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 2), !.
    true.

    See also:

    Maslovs Method in Dogelog Player https://twitter.com/dogelogch/status/1479792480908414979

    Maslovs Method in Dogelog Player
    https://www.facebook.com/groups/dogelog

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sun Jan 9 00:30:12 2022
    One more iteration of our prover:

    Proof systems that are based on the Howard-Curry isomorphism
    and that extract proof terms in the lambda calculus are familiar
    to node dropping. Lambda calculus expressions have a notion
    of variable occurence.

    /* Eta Reduction */
    λx(Mx) ~~> M for x ∉ M

    Variable occurence can then be used similarly to has_usage/2
    to shorten proof terms in the form of lambda expressions. A
    prominent reduction rule is seen in the above that goes by
    the name eta reduction.

    Our provers do extract terms where we store integer sequent
    indexes of used formulas. For the newest variant we generalized
    the terms to alfa, beta, gamma and delta, but we currently do
    not use a generic binder format.

    See also:

    Node Dropping for Maslovs Method https://twitter.com/dogelogch/status/1480091985222451201

    Node Dropping for Maslovs Method
    https://www.facebook.com/groups/dogelog

    Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 16:57:45 UTC+1:
    The problem with the French logician is, that he does not
    get through the thicket of classical logic into the Maslovs method.
    He only shows a translation for intuitionstic logic in the following form:

    (∃xA)* := ∃x !A
    https://girard.perso.math.cnrs.fr/Synsem.pdf

    Given his other definitions for other connectives and quantifiers
    it might work. In his “Table 2: Classical connectives : definition in terms of linear logic” he then repeats this translation.

    I think his translation works since he has exponentation
    elsewhere outside of the quantifier. But the Maslov method shows
    that the outside exponentation in classical connectives is

    superflous, and that we can put the exponentiation in front
    of a certain quantifier.
    Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 14:06:42 UTC+1:
    Now having more fun with Jens Ottens Lean Prover. This
    is a nice little example, where 1 contraction doesn’t work,
    but 2 contractions work:

    ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 1), !.
    fail.
    ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 2), !.
    true.

    See also:

    Maslovs Method in Dogelog Player https://twitter.com/dogelogch/status/1479792480908414979

    Maslovs Method in Dogelog Player
    https://www.facebook.com/groups/dogelog

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Sun Jan 16 17:58:41 2022
    Some papers show calculi with two substitution rules
    where the equation appears as ~(s=t) and flipped
    as ~(t=s). Strange in our take we dont need this,

    only flipped polarity of atomic formulas, this
    is provable with a=b in it:

    1. a = b ∧ p(a) ⇒ p(b)
    2. p(b) (T⇒2 1)
    3. ¬(a = b ∧ p(a)) (T⇒1 1)
    4. ¬p(a) (F∧2 3)
    5. ¬a = b (F∧1 3)
    6. ¬p(b) (F= 5, 4)
    ✓ (ax 6, 2)

    And now with flipped b=a, it works as well:

    1. b = a ∧ p(a) ⇒ p(b)
    2. p(b) (T⇒2 1)
    3. ¬(b = a ∧ p(a)) (T⇒1 1)
    4. ¬p(a) (F∧2 3)
    5. ¬b = a (F∧1 3)
    6. p(a) (F= 5, 2)
    ✓ (ax 4, 6)

    See also:

    First-Order Equality for Maslovs Method https://twitter.com/dogelogch/status/1482885333486379015

    First-Order Equality for Maslovs Method
    https://www.facebook.com/groups/dogelog

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Tue Jan 18 07:57:36 2022
    I did the barber paradox always wrong!
    The biconditional makes it so much easier.

    1. ¬∃y ∀x (s(x, y) ⇔ ¬s(x, x))
    2. ¬∀x (s(x, a) ⇔ ¬s(x, x)) (F∃ 1)
    3. ¬(s(a, a) ⇔ ¬s(a, a)) (F∀ 2)
    4. ¬(s(a, a) ∧ ¬s(a, a)) (F⇔1 3)
    5. ¬¬s(a, a) (F∧2 4)
    6. ¬s(a, a) (F∧1 4)
    7. s(a, a) (F¬ 5)
    ✓ (ax 6, 7)
    4. s(a, a) ∨ ¬s(a, a) (F⇔2 3)
    5. ¬s(a, a) (T∨2 4)
    6. s(a, a) (T∨1 4)
    ✓ (ax 5, 6)

    See also:

    Biconditional Support for Maslovs Method https://twitter.com/dogelogch/status/1483455561031106563

    Biconditional Support for Maslovs Method https://www.facebook.com/groups/dogelog

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Thu Jan 20 06:03:22 2022
    Its a pitty that there is no simple leanTap=, i.e. leanTap= with
    equality. My take is only a few lines, splitting (subst) into (subst1)
    and (subst2) and can run in the browser.

    On the other hand I read:

    The completion-based method for mixed E-unification we
    have described, has been implemented as part of the
    tableau-based theorem prover 3TAP [3]. The implementation
    consists of about 2500 lines of code, written in Quintus Prolog.
    Besides the possibility to prove theorems from predicate logic
    with equality, the E-unification module can be used “stand alone”
    to solve simultaneous mixed E-unification problems.
    https://formal.kastel.kit.edu/beckert/pub/Mixed_Rigid_Universal_E_Unification_CADE94.pdf

    I don’t know how to run 2500 lines of code in the browser.
    And I don’t need some first order equality that would even
    deploy some term order, as is popular in certain term

    rewriting and Knuth Bendix. One interesting test case is this
    one, that works in the browser:

    ?- time(prove0('∀x∀y∀z∀t f(x,y,z,t)=f(y,z,t,x)⇒\ f(a,b,c,d)=f(c,d,a,b)', 9, unicode)), !.
    % Wall 60 ms, gc 0 ms, 1171000 lips

    Thanks to McCarthys trick its quite fast. On monday it still took
    me around 5000 ms, but now its only 60 ms. Wolfgangs Schwartz
    tool can do the same, but interestingly he gets a longer proof with

    more (subst) applications. See also this ticket:

    Does the tree tool search shortest proofs? #11 https://github.com/wo/tpg/issues/11

    Mostowski Collapse schrieb am Dienstag, 18. Januar 2022 um 16:57:38 UTC+1:
    I did the barber paradox always wrong!
    The biconditional makes it so much easier.

    1. ¬∃y ∀x (s(x, y) ⇔ ¬s(x, x))
    2. ¬∀x (s(x, a) ⇔ ¬s(x, x)) (F∃ 1)
    3. ¬(s(a, a) ⇔ ¬s(a, a)) (F∀ 2)
    4. ¬(s(a, a) ∧ ¬s(a, a)) (F⇔1 3)
    5. ¬¬s(a, a) (F∧2 4)
    6. ¬s(a, a) (F∧1 4)
    7. s(a, a) (F¬ 5)
    ✓ (ax 6, 7)
    4. s(a, a) ∨ ¬s(a, a) (F⇔2 3)
    5. ¬s(a, a) (T∨2 4)
    6. s(a, a) (T∨1 4)
    ✓ (ax 5, 6)

    See also:

    Biconditional Support for Maslovs Method https://twitter.com/dogelogch/status/1483455561031106563

    Biconditional Support for Maslovs Method https://www.facebook.com/groups/dogelog

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Thu Jan 20 06:06:03 2022
    See also my blog post on medium.com:

    McCarthys Trick for First Order Equality https://twitter.com/dogelogch/status/1484032442717585409

    McCarthys Trick for First Order Equality https://www.facebook.com/groups/dogelog

    Mostowski Collapse schrieb am Donnerstag, 20. Januar 2022 um 15:03:24 UTC+1:
    Its a pitty that there is no simple leanTap=, i.e. leanTap= with
    equality. My take is only a few lines, splitting (subst) into (subst1)
    and (subst2) and can run in the browser.

    On the other hand I read:

    The completion-based method for mixed E-unification we
    have described, has been implemented as part of the
    tableau-based theorem prover 3TAP [3]. The implementation
    consists of about 2500 lines of code, written in Quintus Prolog.
    Besides the possibility to prove theorems from predicate logic
    with equality, the E-unification module can be used “stand alone”
    to solve simultaneous mixed E-unification problems. https://formal.kastel.kit.edu/beckert/pub/Mixed_Rigid_Universal_E_Unification_CADE94.pdf

    I don’t know how to run 2500 lines of code in the browser.
    And I don’t need some first order equality that would even
    deploy some term order, as is popular in certain term

    rewriting and Knuth Bendix. One interesting test case is this
    one, that works in the browser:

    ?- time(prove0('∀x∀y∀z∀t f(x,y,z,t)=f(y,z,t,x)⇒\ f(a,b,c,d)=f(c,d,a,b)', 9, unicode)), !.
    % Wall 60 ms, gc 0 ms, 1171000 lips

    Thanks to McCarthys trick its quite fast. On monday it still took
    me around 5000 ms, but now its only 60 ms. Wolfgangs Schwartz
    tool can do the same, but interestingly he gets a longer proof with

    more (subst) applications. See also this ticket:

    Does the tree tool search shortest proofs? #11 https://github.com/wo/tpg/issues/11
    Mostowski Collapse schrieb am Dienstag, 18. Januar 2022 um 16:57:38 UTC+1:
    I did the barber paradox always wrong!
    The biconditional makes it so much easier.

    1. ¬∃y ∀x (s(x, y) ⇔ ¬s(x, x))
    2. ¬∀x (s(x, a) ⇔ ¬s(x, x)) (F∃ 1)
    3. ¬(s(a, a) ⇔ ¬s(a, a)) (F∀ 2)
    4. ¬(s(a, a) ∧ ¬s(a, a)) (F⇔1 3)
    5. ¬¬s(a, a) (F∧2 4)
    6. ¬s(a, a) (F∧1 4)
    7. s(a, a) (F¬ 5)
    ✓ (ax 6, 7)
    4. s(a, a) ∨ ¬s(a, a) (F⇔2 3)
    5. ¬s(a, a) (T∨2 4)
    6. s(a, a) (T∨1 4)
    ✓ (ax 5, 6)

    See also:

    Biconditional Support for Maslovs Method https://twitter.com/dogelogch/status/1483455561031106563

    Biconditional Support for Maslovs Method https://www.facebook.com/groups/dogelog

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sat Jan 22 09:52:14 2022
    Here is a poket McCarthy for propositional logic only.
    It can also do Joseph Vidal-Rossets antisequent (asq):

    :- op( 500, fy, ~). % negation
    :- op(1000, xfy, &). % conjunction
    :- op(1100, xfy, '|'). % disjunction
    :- op(1110, xfy, =>). % conditional
    :- op(1120, xfy, <=>). % biconditional

    prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
    prove(G>[~A,B|D],P).
    prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
    prove(G>[A,B|D],P).
    /* double negation */
    prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
    prove(G>[A|D],P).
    prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
    prove(G>[~A,~B|D],P).

    prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
    prove(G>[~A,B|D],P1),
    prove(G>[A,~B|D], P2).
    prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
    prove(G>[~A,~B|D],P1),
    prove(G>[A,B|D],P2).
    prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
    prove(G>[A|D],P1),
    prove(G>[~B|D],P2).
    prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
    prove(G>[A|D],P1),
    prove(G>[B|D],P2).
    prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
    prove(G>[~A|D],P1),
    prove(G>[~B|D],P2).

    prove(G>[A|D], ax(G>[A|D], A)):-
    member(B,G), A==B, !.

    /* next */
    prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
    prove([A|G]>D,P).
    prove(G>[A|D], lneg(G>[A|D], P)) :- !,
    prove([~A|G]>D,P).
    prove(G>[], asq(G>[], asq)).

    provable(F,P):-
    prove([]>[F],P).

    member(E, [E|_]).
    member(E, [_|Xs]) :-
    member(E, Xs).

    Mostowski Collapse schrieb am Donnerstag, 20. Januar 2022 um 15:06:05 UTC+1:
    See also my blog post on medium.com:

    McCarthys Trick for First Order Equality https://twitter.com/dogelogch/status/1484032442717585409

    McCarthys Trick for First Order Equality https://www.facebook.com/groups/dogelog

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sat Jan 22 18:58:38 2022
    Why does Jens Otten automatic reordering preprocessing
    give some bang? Now I get for Pelletier problem 71:

    /* Joseph Vidal-Rossets LeanSeq, from his web site */
    ?- test.
    % 54,202,362 inferences, 4.969 CPU in 5.017 seconds
    (99% CPU, 10908954 Lips)
    true. https://www.vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html

    /* My McCarthy */
    ?- test2.
    % 8,814,592 inferences, 1.099 CPU in 1.123 seconds
    (98% CPU, 8019776 Lips)
    true.

    I think this is because rbicond is more symmetric,
    in my new McCarthy it is now:

    prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
    prove(G>[~A,B|D],P1),
    prove(G>[A,~B|D], P2).

    On the other hand Joseph Vidal-Rossets LeanSeq
    has the following rbicond rule:

    prove(G>D, rbicond(G>D,P1,P2)):-
    select((A<=>B),D,D1),!,
    prove([A|G]>[B|D1],P1),
    prove([B|G]>[A|D1], P2).

    But this works only for Pelletier problem 71.
    The rule is still quite static, and doesn't

    do any reordering.

    Mostowski Collapse schrieb:
    Here is a poket McCarthy for propositional logic only.
    It can also do Joseph Vidal-Rossets antisequent (asq):

    :- op( 500, fy, ~). % negation
    :- op(1000, xfy, &). % conjunction
    :- op(1100, xfy, '|'). % disjunction
    :- op(1110, xfy, =>). % conditional
    :- op(1120, xfy, <=>). % biconditional

    prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
    prove(G>[~A,B|D],P).
    prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
    prove(G>[A,B|D],P).
    /* double negation */
    prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
    prove(G>[A|D],P).
    prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
    prove(G>[~A,~B|D],P).

    prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
    prove(G>[~A,B|D],P1),
    prove(G>[A,~B|D], P2).
    prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
    prove(G>[~A,~B|D],P1),
    prove(G>[A,B|D],P2).
    prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
    prove(G>[A|D],P1),
    prove(G>[~B|D],P2).
    prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
    prove(G>[A|D],P1),
    prove(G>[B|D],P2).
    prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
    prove(G>[~A|D],P1),
    prove(G>[~B|D],P2).

    prove(G>[A|D], ax(G>[A|D], A)):-
    member(B,G), A==B, !.

    /* next */
    prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
    prove([A|G]>D,P).
    prove(G>[A|D], lneg(G>[A|D], P)) :- !,
    prove([~A|G]>D,P).
    prove(G>[], asq(G>[], asq)).

    provable(F,P):-
    prove([]>[F],P).

    member(E, [E|_]).
    member(E, [_|Xs]) :-
    member(E, Xs).

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sun Jan 23 01:32:16 2022
    There is a bug in nff_pure.pl by Jens Otten. This here:

    Fml = (A <=> B) -> Fml1 = ((A & B) ; (~A & ~B));
    Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) ; (~A & B)) ), !,

    Should read, so that it runs in a wider variety of Prolog systems:

    Fml = (A <=> B) -> Fml1 = ((A & B) | (~A & ~B));
    Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) | (~A & B)) ), !,

    And we can now try Pelletier problem 71, and it doesn’t work:

    % 88,652,639 inferences, 13.734 CPU in 13.999 seconds
    (98% CPU, 6454800 Lips)
    ERROR: Stack limit (1.0Gb) exceeded

    Strange...

    Mostowski Collapse schrieb:
    Why does Jens Otten automatic reordering preprocessing
    give some bang? Now I get for Pelletier problem 71:

    /* Joseph Vidal-Rossets LeanSeq, from his web site */
    ?- test.
    % 54,202,362 inferences, 4.969 CPU in 5.017 seconds
    (99% CPU, 10908954 Lips)
    true. https://www.vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html


    /* My McCarthy */
    ?- test2.
    % 8,814,592 inferences, 1.099 CPU in 1.123 seconds
    (98% CPU, 8019776 Lips)
    true.

    I think this is because rbicond is more symmetric,
    in my new McCarthy it is now:

    prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
            prove(G>[~A,B|D],P1),
            prove(G>[A,~B|D], P2).

    On the other hand Joseph Vidal-Rossets LeanSeq
    has the following rbicond rule:

    prove(G>D, rbicond(G>D,P1,P2)):-
            select((A<=>B),D,D1),!,
            prove([A|G]>[B|D1],P1),
            prove([B|G]>[A|D1], P2).

    But this works only for Pelletier problem 71.
    The rule is still quite static, and doesn't

    do any reordering.

    Mostowski Collapse schrieb:
    Here is a poket McCarthy for propositional logic only.
    It can also do Joseph Vidal-Rossets antisequent (asq):
    :- op( 500, fy, ~).     % negation
    :- op(1000, xfy, &).    % conjunction
    :- op(1100, xfy, '|').  % disjunction
    :- op(1110, xfy, =>).   % conditional
    :- op(1120, xfy, <=>).  % biconditional

    prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
            prove(G>[~A,B|D],P).
    prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
            prove(G>[A,B|D],P).
    /* double negation */
    prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
            prove(G>[A|D],P).
    prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
            prove(G>[~A,~B|D],P).

    prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
            prove(G>[~A,B|D],P1),
            prove(G>[A,~B|D], P2).
    prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
            prove(G>[~A,~B|D],P1),
            prove(G>[A,B|D],P2).
    prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
            prove(G>[A|D],P1),
            prove(G>[~B|D],P2).
    prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
            prove(G>[A|D],P1),
            prove(G>[B|D],P2).
    prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
            prove(G>[~A|D],P1),
            prove(G>[~B|D],P2).

    prove(G>[A|D], ax(G>[A|D], A)):-
            member(B,G), A==B, !.

    /* next */
    prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
            prove([A|G]>D,P).
    prove(G>[A|D], lneg(G>[A|D], P)) :- !,
            prove([~A|G]>D,P).
    prove(G>[], asq(G>[], asq)).

    provable(F,P):-
            prove([]>[F],P).

    member(E, [E|_]).
    member(E, [_|Xs]) :-
       member(E, Xs).

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sun Jan 23 07:54:34 2022
    If I paste my poket McCarthy into Joseph Vidal-Rossets web
    page, I can reproduce the example from page 7 of this paper:

    leanTAP Revisited
    Melvin Fitting - March 13, 1997 http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36.3518&rep=rep1&type=pdf

    Simply use this here:
    ?- provable(((~p & q) | p), Proof).

    The red color shows where the proof tree ends in Γ |- .
    Joseph Vidal-Rosset could make a fork of his website,
    that provides poket McCarthy directly for experimentation,

    also using better proof tree lables. My own web site
    does not yet show some red color. Thats a little too
    early. First need to get my head around model finding

    from tableaux for the non-propositional case...

    Mostowski Collapse schrieb am Sonntag, 23. Januar 2022 um 01:32:19 UTC+1:
    There is a bug in nff_pure.pl by Jens Otten. This here:

    Fml = (A <=> B) -> Fml1 = ((A & B) ; (~A & ~B));
    Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) ; (~A & B)) ), !,

    Should read, so that it runs in a wider variety of Prolog systems:

    Fml = (A <=> B) -> Fml1 = ((A & B) | (~A & ~B));
    Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) | (~A & B)) ), !,

    And we can now try Pelletier problem 71, and it doesn’t work:

    % 88,652,639 inferences, 13.734 CPU in 13.999 seconds
    (98% CPU, 6454800 Lips)
    ERROR: Stack limit (1.0Gb) exceeded

    Strange...

    Mostowski Collapse schrieb:
    Why does Jens Otten automatic reordering preprocessing
    give some bang? Now I get for Pelletier problem 71:

    /* Joseph Vidal-Rossets LeanSeq, from his web site */
    ?- test.
    % 54,202,362 inferences, 4.969 CPU in 5.017 seconds
    (99% CPU, 10908954 Lips)
    true. https://www.vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html


    /* My McCarthy */
    ?- test2.
    % 8,814,592 inferences, 1.099 CPU in 1.123 seconds
    (98% CPU, 8019776 Lips)
    true.

    I think this is because rbicond is more symmetric,
    in my new McCarthy it is now:

    prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
    prove(G>[~A,B|D],P1),
    prove(G>[A,~B|D], P2).

    On the other hand Joseph Vidal-Rossets LeanSeq
    has the following rbicond rule:

    prove(G>D, rbicond(G>D,P1,P2)):-
    select((A<=>B),D,D1),!,
    prove([A|G]>[B|D1],P1),
    prove([B|G]>[A|D1], P2).

    But this works only for Pelletier problem 71.
    The rule is still quite static, and doesn't

    do any reordering.

    Mostowski Collapse schrieb:
    Here is a poket McCarthy for propositional logic only.
    It can also do Joseph Vidal-Rossets antisequent (asq):
    :- op( 500, fy, ~). % negation
    :- op(1000, xfy, &). % conjunction
    :- op(1100, xfy, '|'). % disjunction
    :- op(1110, xfy, =>). % conditional
    :- op(1120, xfy, <=>). % biconditional

    prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
    prove(G>[~A,B|D],P).
    prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
    prove(G>[A,B|D],P).
    /* double negation */
    prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
    prove(G>[A|D],P).
    prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
    prove(G>[~A,~B|D],P).

    prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
    prove(G>[~A,B|D],P1),
    prove(G>[A,~B|D], P2).
    prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
    prove(G>[~A,~B|D],P1),
    prove(G>[A,B|D],P2).
    prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
    prove(G>[A|D],P1),
    prove(G>[~B|D],P2).
    prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
    prove(G>[A|D],P1),
    prove(G>[B|D],P2).
    prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
    prove(G>[~A|D],P1),
    prove(G>[~B|D],P2).

    prove(G>[A|D], ax(G>[A|D], A)):-
    member(B,G), A==B, !.

    /* next */
    prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
    prove([A|G]>D,P).
    prove(G>[A|D], lneg(G>[A|D], P)) :- !,
    prove([~A|G]>D,P).
    prove(G>[], asq(G>[], asq)).

    provable(F,P):-
    prove([]>[F],P).

    member(E, [E|_]).
    member(E, [_|Xs]) :-
    member(E, Xs).

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sun Jan 23 13:02:05 2022
    This one is much shorter, 6 pages code by Triska, 2015:
    Prolog implementation of the Knuth-Bendix completion procedure https://www.metalevel.at/trs/

    But is it lean? Something shorter maybe?

    Mostowski Collapse schrieb am Donnerstag, 20. Januar 2022 um 15:03:24 UTC+1:
    The completion-based method for mixed E-unification we
    have described, has been implemented as part of the
    tableau-based theorem prover 3TAP [3]. The implementation
    consists of about 2500 lines of code, written in Quintus Prolog.
    Besides the possibility to prove theorems from predicate logic
    with equality, the E-unification module can be used “stand alone”
    to solve simultaneous mixed E-unification problems. https://formal.kastel.kit.edu/beckert/pub/Mixed_Rigid_Universal_E_Unification_CADE94.pdf

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Mon Jan 24 02:38:18 2022
    Melvin Fitting uses the anti-sequents in a semantic completeness
    argument. This then explains how validity proving is relatated to SAT
    solving. Actually to be precise, validity is UNSAT. For randomized

    algorithms there are complexity results for (SAT, ε-UNSAT). But these
    results only appeared in recent years.

    Mostowski Collapse schrieb am Sonntag, 23. Januar 2022 um 16:54:35 UTC+1:
    If I paste my poket McCarthy into Joseph Vidal-Rossets web
    page, I can reproduce the example from page 7 of this paper:

    leanTAP Revisited
    Melvin Fitting - March 13, 1997 http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36.3518&rep=rep1&type=pdf

    Simply use this here:
    ?- provable(((~p & q) | p), Proof).

    The red color shows where the proof tree ends in Γ |- .
    Joseph Vidal-Rosset could make a fork of his website,
    that provides poket McCarthy directly for experimentation,

    also using better proof tree lables. My own web site
    does not yet show some red color. Thats a little too
    early. First need to get my head around model finding

    from tableaux for the non-propositional case...
    Mostowski Collapse schrieb am Sonntag, 23. Januar 2022 um 01:32:19 UTC+1:
    There is a bug in nff_pure.pl by Jens Otten. This here:

    Fml = (A <=> B) -> Fml1 = ((A & B) ; (~A & ~B));
    Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) ; (~A & B)) ), !,

    Should read, so that it runs in a wider variety of Prolog systems:

    Fml = (A <=> B) -> Fml1 = ((A & B) | (~A & ~B));
    Fml = ~((A<=>B)) -> Fml1 = ((A & ~B) | (~A & B)) ), !,

    And we can now try Pelletier problem 71, and it doesn’t work:

    % 88,652,639 inferences, 13.734 CPU in 13.999 seconds
    (98% CPU, 6454800 Lips)
    ERROR: Stack limit (1.0Gb) exceeded

    Strange...

    Mostowski Collapse schrieb:
    Why does Jens Otten automatic reordering preprocessing
    give some bang? Now I get for Pelletier problem 71:

    /* Joseph Vidal-Rossets LeanSeq, from his web site */
    ?- test.
    % 54,202,362 inferences, 4.969 CPU in 5.017 seconds
    (99% CPU, 10908954 Lips)
    true. https://www.vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html


    /* My McCarthy */
    ?- test2.
    % 8,814,592 inferences, 1.099 CPU in 1.123 seconds
    (98% CPU, 8019776 Lips)
    true.

    I think this is because rbicond is more symmetric,
    in my new McCarthy it is now:

    prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !, prove(G>[~A,B|D],P1),
    prove(G>[A,~B|D], P2).

    On the other hand Joseph Vidal-Rossets LeanSeq
    has the following rbicond rule:

    prove(G>D, rbicond(G>D,P1,P2)):-
    select((A<=>B),D,D1),!,
    prove([A|G]>[B|D1],P1),
    prove([B|G]>[A|D1], P2).

    But this works only for Pelletier problem 71.
    The rule is still quite static, and doesn't

    do any reordering.

    Mostowski Collapse schrieb:
    Here is a poket McCarthy for propositional logic only.
    It can also do Joseph Vidal-Rossets antisequent (asq):
    :- op( 500, fy, ~). % negation
    :- op(1000, xfy, &). % conjunction
    :- op(1100, xfy, '|'). % disjunction
    :- op(1110, xfy, =>). % conditional
    :- op(1120, xfy, <=>). % biconditional

    prove(G>[(A=>B)|D], rcond(G>[(A=>B)|D],P)):- !,
    prove(G>[~A,B|D],P).
    prove(G>[(A|B)|D], ror(G>[(A|B)|D], P)):- !,
    prove(G>[A,B|D],P).
    /* double negation */
    prove(G>[~ ~A|D], rneg(G>[~ ~A|D],P)):- !,
    prove(G>[A|D],P).
    prove(G>[~ (A&B)|D], land(G>[~ (A&B)|D],P)):- !,
    prove(G>[~A,~B|D],P).

    prove(G>[(A<=>B)|D], rbicond(G>[(A<=>B)|D],P1,P2)):- !,
    prove(G>[~A,B|D],P1),
    prove(G>[A,~B|D], P2).
    prove(G>[~ (A<=>B)|D], lbicond(G>[~ (A<=>B)|D], P1,P2)):- !,
    prove(G>[~A,~B|D],P1),
    prove(G>[A,B|D],P2).
    prove(G>[~ (A=>B)|D], lcond(G>[~ (A=>B)|D],P1,P2)):- !,
    prove(G>[A|D],P1),
    prove(G>[~B|D],P2).
    prove(G>[(A&B)|D], rand(G>[(A&B)|D],P1,P2)):- !,
    prove(G>[A|D],P1),
    prove(G>[B|D],P2).
    prove(G>[~ (A|B)|D], lor(G>[~ (A|B)|D], P1,P2)):- !,
    prove(G>[~A|D],P1),
    prove(G>[~B|D],P2).

    prove(G>[A|D], ax(G>[A|D], A)):-
    member(B,G), A==B, !.

    /* next */
    prove(G>[~A|D], lneg(G>[~A|D], P)) :- !,
    prove([A|G]>D,P).
    prove(G>[A|D], lneg(G>[A|D], P)) :- !,
    prove([~A|G]>D,P).
    prove(G>[], asq(G>[], asq)).

    provable(F,P):-
    prove([]>[F],P).

    member(E, [E|_]).
    member(E, [_|Xs]) :-
    member(E, Xs).

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sun Jan 30 12:15:07 2022
    I guess there is some literature that explains everything. On the
    other hand some Prolog experimentation could maybe help
    increase intuition. leanseq_v5.pl first, and I get, limiting the

    depth to 10, it already takes quite some time with 10 in this
    automated prover which doesn’t have much optimizations:

    % leanseq_v5.pl compiled 0.00 sec, 17 clauses
    ?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
    iteration 1
    iteration 2
    iteration 3
    iteration 4
    iteration 5
    iteration 6
    iteration 7
    iteration 8
    iteration 9
    iteration 10
    false.

    Now the faulty leanseq_v5f.pl, where the Skolem function
    is replaced by only a Skolem constant:

    % leanseq_v5f.pl compiled 0.00 sec, 17 clauses
    ?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
    iteration 1
    iteration 2
    true

    Mostowski Collapse schrieb am Sonntag, 30. Januar 2022 um 21:11:01 UTC+1:
    Today a little show of what can go wrong: Question
    was why does Jens Otten leanseq_v5.pl use this:

    prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !, copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
    J1 is J+1,
    prove(G > [A1|D1],FV,I,J1,K).

    And not this:

    prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !, copy_term((X:A,FV),(f_sk(J):A1,FV)),
    J1 is J+1,
    prove(G > [A1|D1],FV,I,J1,K).

    The offending test case is this here:

    ∀y∃xFxy → ∃z∀tFzt is invalid.
    Countermodel:
    Domain: { 0, 1 }
    F: { (0,0), (1,1) }
    https://www.umsu.de/trees/#~6y~7xFxy~5~7z~6tFzt

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Sun Jan 30 12:10:59 2022
    Today a little show of what can go wrong: Question
    was why does Jens Otten leanseq_v5.pl use this:

    prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !,
    copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
    J1 is J+1,
    prove(G > [A1|D1],FV,I,J1,K).

    And not this:

    prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !,
    copy_term((X:A,FV),(f_sk(J):A1,FV)),
    J1 is J+1,
    prove(G > [A1|D1],FV,I,J1,K).

    The offending test case is this here:

    ∀y∃xFxy → ∃z∀tFzt is invalid.
    Countermodel:
    Domain: { 0, 1 }
    F: { (0,0), (1,1) }
    https://www.umsu.de/trees/#~6y~7xFxy~5~7z~6tFzt

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sun Jan 30 12:21:23 2022
    nyway, because nobody has time to wait for ZDD provide a model
    finder or to wait that theorem prover has finished its infinitely many iterations, to show that a formula isn’t provable.

    I started publishing a counter model finder for my new Dogelog player.
    This is a first beginning, more posts will follow.

    Boole’s Method from 1847 in Dogelog Player https://twitter.com/dogelogch/status/1487845636993134596

    Boole’s Method from 1847 in Dogelog Player https://www.facebook.com/groups/dogelog

    Mostowski Collapse schrieb am Sonntag, 30. Januar 2022 um 21:15:08 UTC+1:
    I guess there is some literature that explains everything. On the
    other hand some Prolog experimentation could maybe help
    increase intuition. leanseq_v5.pl first, and I get, limiting the

    depth to 10, it already takes quite some time with 10 in this
    automated prover which doesn’t have much optimizations:

    % leanseq_v5.pl compiled 0.00 sec, 17 clauses
    ?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
    iteration 1
    iteration 2
    iteration 3
    iteration 4
    iteration 5
    iteration 6
    iteration 7
    iteration 8
    iteration 9
    iteration 10
    false.

    Now the faulty leanseq_v5f.pl, where the Skolem function
    is replaced by only a Skolem constant:

    % leanseq_v5f.pl compiled 0.00 sec, 17 clauses
    ?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
    iteration 1
    iteration 2
    true
    Mostowski Collapse schrieb am Sonntag, 30. Januar 2022 um 21:11:01 UTC+1:
    Today a little show of what can go wrong: Question
    was why does Jens Otten leanseq_v5.pl use this:

    prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !, copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
    J1 is J+1,
    prove(G > [A1|D1],FV,I,J1,K).

    And not this:

    prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !, copy_term((X:A,FV),(f_sk(J):A1,FV)),
    J1 is J+1,
    prove(G > [A1|D1],FV,I,J1,K).

    The offending test case is this here:

    ∀y∃xFxy → ∃z∀tFzt is invalid.
    Countermodel:
    Domain: { 0, 1 }
    F: { (0,0), (1,1) }
    https://www.umsu.de/trees/#~6y~7xFxy~5~7z~6tFzt

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Tue Feb 8 03:28:04 2022
    You can run leanTap in Dogelog player in the browser. For the
    simple problems among Pelletier 17-46 I get the following
    results (100 iterations, browser was Chrome no async/await):

    System Time
    Tau Prolog 323’000
    Dogelog Player 2’441
    Formerly Jekejeke 811
    SWI 299

    Will post a link to a fork later. I want to compare different normal
    forms, but still struggling with optimal way to compute prenex and
    mini-scope. Too large design space, so slow progress.

    The simple problems are:

    17 18 19 20 21 22 23 24 27 28 29 30 31 32 33 35 36 39 40 41 42 44

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Thu Feb 10 08:29:44 2022
    Thats the code of the two provers. First leanTap you might easily recognize:

    prove((A|B),UnExp,Lits,FreeV,VarLim) :- !,
    prove(A,[B|UnExp],Lits,FreeV,VarLim). prove((A&B),UnExp,Lits,FreeV,VarLim) :- !,
    prove(A,UnExp,Lits,FreeV,VarLim),
    prove(B,UnExp,Lits,FreeV,VarLim). prove((?[X]:Fml),UnExp,Lits,FreeV,VarLim) :- VarLim>0, !,
    copy_term((X,Fml,FreeV),(X1,Fml1,FreeV)),
    append(UnExp,[(?[X]:Fml)],UnExp1),
    VarLim2 is VarLim-1,
    prove(Fml1,UnExp1,Lits,[X1|FreeV],VarLim2).
    prove(Lit,_,Lits,_,_) :-
    \+ Lit = (?_),
    member(L,Lits), unify_with_occurs_check(Lit,L). prove(Fml,[Next|UnExp],Lits,FreeV,VarLim) :-
    opposite(Fml, Fml1),
    prove(Next,UnExp,[Fml1|Lits],FreeV,VarLim).

    And here leanSeq, which expects NNF and does literal saturation:

    prove((A|B),UnExp,Lits,FreeV,VarLim,J,K) :- !,
    prove(A,[B|UnExp],Lits,FreeV,VarLim,J,K). prove((A&B),UnExp,Lits,FreeV,VarLim,J,K) :- !,
    prove(A,UnExp,Lits,FreeV,VarLim,J,H),
    prove(B,UnExp,Lits,FreeV,VarLim,H,K). prove((![X]:Fml),UnExp,Lits,FreeV,VarLim,J,K) :- !,
    copy_term((X:Fml,FreeV),(h(J,FreeV):Fml1,FreeV)),
    J1 is J+1,
    prove(Fml1,UnExp,Lits,FreeV,VarLim,J1,K). prove(Lit,_,Lits,_,_,J,J) :-
    \+ Lit = (?_),
    member(L,Lits),
    unify_with_occurs_check(Lit,L). prove(Fml,[Next|UnExp],Lits,FreeV,VarLim,J,K) :- !,
    opposite(Fml, Fml1),
    prove(Next,UnExp,[Fml1|Lits],FreeV,VarLim,J,K).

    % we are saturated
    prove(Fml,[],Lits,FreeV,VarLim,J,K) :- VarLim>0, opposite(Fml, L),
    member(H,[L|Lits]),
    H = ~ (?_),
    opposite(H,M),
    block(M,[L|Lits],FreeV,VarLim,J,K).

    % quantifier block
    block((?[X]:Fml),Lits,FreeV,VarLim,J,K) :- !, VarLim>0,
    copy_term((X:Fml,FreeV),(Y:Fml1,FreeV)),
    VarLim2 is VarLim-1,
    block(Fml1,Lits,[Y|FreeV],VarLim2,J,K). block(Fml,Lits,FreeV,VarLim,J,K) :-
    prove(Fml,[],Lits,FreeV,VarLim,J,K).

    The new leanSeq has a little more backtracking in the handling of (?[X]:Fml), block/6 is mitigating the problem a little bit. Overall the penality seems to be
    not so high, measured by the simple Pelletier problems.

    Mostowski Collapse schrieb am Donnerstag, 10. Februar 2022 um 17:27:55 UTC+1:
    Now I have obtained a new result, leanTap is not really needed,
    leanSeq could also do? I was using negation normal form with leanSeq,
    and now leanSeq is also extremly fast. Maybe because of some indexing?

    I used a leanSeq variant that saturates the literals before it tries the quantifier.
    When I compare the two, there is not anymore much difference between leanSeq and leanTap. Only the new leanSeq would allow easy proof extraction:

    /* leanTap */
    ?- time((between(1,100,_), test(time), fail; true)).
    % 3,011,100 inferences, 0.203 CPU in 0.206 seconds (99% CPU, 14823877 Lips) true.

    /* leanSeq+NNF+literal saturation */
    ?- time((between(1,100,_), test(time), fail; true)).
    % 8,858,800 inferences, 0.844 CPU in 0.853 seconds (99% CPU, 10499319 Lips) true.

    The difference is only a factor of ca. 4. Not that bad. I used a simple negation normal form without any reordering for both.
    Mostowski Collapse schrieb am Dienstag, 8. Februar 2022 um 12:28:05 UTC+1:
    You can run leanTap in Dogelog player in the browser. For the
    simple problems among Pelletier 17-46 I get the following
    results (100 iterations, browser was Chrome no async/await):

    System Time
    Tau Prolog 323’000
    Dogelog Player 2’441
    Formerly Jekejeke 811
    SWI 299

    Will post a link to a fork later. I want to compare different normal forms, but still struggling with optimal way to compute prenex and mini-scope. Too large design space, so slow progress.

    The simple problems are:

    17 18 19 20 21 22 23 24 27 28 29 30 31 32 33 35 36 39 40 41 42 44

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Thu Feb 10 08:27:54 2022
    Now I have obtained a new result, leanTap is not really needed,
    leanSeq could also do? I was using negation normal form with leanSeq,
    and now leanSeq is also extremly fast. Maybe because of some indexing?

    I used a leanSeq variant that saturates the literals before it tries the quantifier.
    When I compare the two, there is not anymore much difference between leanSeq and leanTap. Only the new leanSeq would allow easy proof extraction:

    /* leanTap */
    ?- time((between(1,100,_), test(time), fail; true)).
    % 3,011,100 inferences, 0.203 CPU in 0.206 seconds (99% CPU, 14823877 Lips) true.

    /* leanSeq+NNF+literal saturation */
    ?- time((between(1,100,_), test(time), fail; true)).
    % 8,858,800 inferences, 0.844 CPU in 0.853 seconds (99% CPU, 10499319 Lips) true.

    The difference is only a factor of ca. 4. Not that bad. I used a simple negation normal form without any reordering for both.

    Mostowski Collapse schrieb am Dienstag, 8. Februar 2022 um 12:28:05 UTC+1:
    You can run leanTap in Dogelog player in the browser. For the
    simple problems among Pelletier 17-46 I get the following
    results (100 iterations, browser was Chrome no async/await):

    System Time
    Tau Prolog 323’000
    Dogelog Player 2’441
    Formerly Jekejeke 811
    SWI 299

    Will post a link to a fork later. I want to compare different normal
    forms, but still struggling with optimal way to compute prenex and mini-scope. Too large design space, so slow progress.

    The simple problems are:

    17 18 19 20 21 22 23 24 27 28 29 30 31 32 33 35 36 39 40 41 42 44

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Sat Feb 12 05:02:23 2022
    Happy Birthday Jacques Herbrand

    February 12th, 1908: French mathematician, worked in
    math. logic and field theory, Jacques Herbrand, was born. https://twitter.com/sc_k/status/9011037015

    Lectures on Jacques Herbrand as a Logician
    https://arxiv.org/abs/0902.4682

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Mon Feb 14 03:59:21 2022
    Now I managed to add first order equality to
    leanTap. Here is a comparison:

    leanSeq= vs leanTap= in Dogelog Player https://twitter.com/dogelogch/status/1492869014267248641

    leanSeq= vs leanTap= in Dogelog Player
    https://www.facebook.com/groups/dogelog

    Have Fun!

    Mostowski Collapse schrieb am Samstag, 12. Februar 2022 um 14:02:24 UTC+1:
    Happy Birthday Jacques Herbrand

    February 12th, 1908: French mathematician, worked in
    math. logic and field theory, Jacques Herbrand, was born. https://twitter.com/sc_k/status/9011037015

    Lectures on Jacques Herbrand as a Logician
    https://arxiv.org/abs/0902.4682

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Mon Feb 14 09:35:34 2022
    The next step in proof assistants would be a theorem prover
    with an inconsistent logic that when programs are extracted,
    these programs will make Zucks metaverse collapse (or USA
    think Russia is invading Ukraine, etc.. etc.. as you like)

    Just like Jean Tinguely:

    He then began to construct his first truly sophisticated kinetic
    sculptures, which he termed métaméchaniques, or metamechanicals.
    These were robotlike contraptions constructed of wire and sheet
    metal, the constituent parts of which moved or spun at varying
    speeds. Further innovations on Tinguely’s part in the mid- and
    late 1950s led to a series of sculptures entitled “Machines à
    peindre” (“Painting Machines”); these robotlike machines continuously painted pictures of abstract patterns to the accompaniment of self-
    produced sounds and noxious odours. The 8-foot-long “painting
    machine” that Tinguely set up at the first Paris Biennale in 1959
    produced some 40,000 different paintings for exhibition visitors
    who inserted a coin in its slot.

    Tinguely was meanwhile becoming obsessed with the concept of
    destruction as a means of achieving the “dematerialization” of his
    works of art. In 1960 he created a sensation with his first large self- destroying sculpture, the 27-foot-high metamatic entitled “Homage
    to New York,” whose public suicide he demonstrated at the Museum
    of Modern Art in New York City. The event was a fiasco, with the
    complicated assemblage of motors and wheels failing to operate
    (i.e., destroy itself) properly; it had to be dispatched by city firemen
    with axes after having started a fire. But Tinguely’s next two self- destroying machines, entitled “Study for an End of the World,” performed more successfully, detonating themselves with considerable
    amounts of explosives. https://www.britannica.com/biography/Jean-Tinguely#ref290920

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Mon Feb 14 10:42:06 2022
    A well suited candidate for such self destroing machines
    is miniKanren. In the case of miniKanren, it does already
    self destroy during theorem proving. I have no clue

    what they are reporting here (in milliseconds):

    Pelletier #34:
    leanTap: 199'129.0
    mKleanTap: 7'272.9
    αleanTap: 8493.5
    Near J.P., Byrd W.E., Friedman D.P. (2008) αleanTAP: A Declarative
    Theorem Prover for First-Order Classical Logic. In: Garcia de la Banda
    M., Pontelli E. (eds) Logic Programming. ICLP 2008. Lecture Notes in
    Computer Science, vol 5366. Springer, Berlin, Heidelberg. http://webyrd.net/alphaleantap/alphatap.pdf

    Maybe they used a version with an unfavorable biconditional
    realization or some other nonsense. In my fluffy Dogelog player
    I get here and now on my slow MacOSX machine:

    ?- time(prove(((?[X]:![Y]:(p(X) <=> p(Y)) <=> (?[Z]:q(Z) <=> ![T]:q(T)))
    <=> (?[U]:![V]:(q(U) <=> q(V)) <=> (?[S]:p(S) <=> ![R]:p(R)))), tap, I)).
    % Wall 1385 ms, gc 5 ms, 2342329 lips
    I = 5. http://www.xlog.ch/izytab/doclet/docs/18_live/32_bik2022/paste36/package.html

    Anybody can reproduce the same result in his own
    browser. It rather tells me that the miniKanren solutions
    are uselessly slow...

    Pelletier 34 has an errata, it says Problem # 34: The third
    occurrence of 'P' should be 'Q'. This is in my TPTP form q(T).
    Me thinks the formula is correct.

    Its even a much less a challenge for leanSeq:

    ?- time(prove(((?[X]:![Y]:(p(X) <=> p(Y)) <=> (?[Z]:q(Z) <=> ![T]:q(T)))
    <=> (?[U]:![V]:(q(U) <=> q(V)) <=> (?[S]:p(S) <=> ![R]:p(R)))), seq, I)).
    % Wall 29 ms, gc 1 ms, 1056620 lips
    I = 2.

    If I have time I will double check a proof tree...

    Mostowski Collapse schrieb am Montag, 14. Februar 2022 um 18:35:36 UTC+1:
    with axes after having started a fire. But Tinguely’s next two self- destroying machines, entitled “Study for an End of the World,” performed more successfully, detonating themselves with considerable https://www.britannica.com/biography/Jean-Tinguely#ref290920

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Sat Jul 9 01:12:36 2022
    Probably something that would make Alain
    Colmerauer happy. By way of EricGT on
    SWI-Prolog discourse:

    "Prolog broke into the top 20 again a few months ago
    (should have captured it then for historical use).
    As of June 2022 it is still at 20."
    https://www.tiobe.com/tiobe-index/

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sat Jul 9 01:36:48 2022
    I guess we can overtake Ruby, which is on 19,
    if we provide some "Prolog on Rails". Anybody up to it?

    Mostowski Collapse schrieb am Samstag, 9. Juli 2022 um 10:12:37 UTC+2:
    Probably something that would make Alain
    Colmerauer happy. By way of EricGT on
    SWI-Prolog discourse:

    "Prolog broke into the top 20 again a few months ago
    (should have captured it then for historical use).
    As of June 2022 it is still at 20."
    https://www.tiobe.com/tiobe-index/

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Sat Jul 9 01:49:11 2022
    (P.S.: The idea would be to provide and base the Rails
    functionality in 100% Prolog programming language)

    Mostowski Collapse schrieb am Samstag, 9. Juli 2022 um 10:36:49 UTC+2:
    I guess we can overtake Ruby, which is on 19,
    if we provide some "Prolog on Rails". Anybody up to it?

    Mostowski Collapse schrieb am Samstag, 9. Juli 2022 um 10:12:37 UTC+2:
    Probably something that would make Alain
    Colmerauer happy. By way of EricGT on
    SWI-Prolog discourse:

    "Prolog broke into the top 20 again a few months ago
    (should have captured it then for historical use).
    As of June 2022 it is still at 20."
    https://www.tiobe.com/tiobe-index/

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Wed Sep 14 09:38:56 2022
    Disclaimer: Source of OSTINT, 9gag.com head quarters.
    (one should not praise the morning before the evening)

    Mostowski Collapse schrieb am Mittwoch, 14. September 2022 um 18:25:25 UTC+2:
    You can learn a lot from this animal, for example:

    - Rule 1 of speedy exit:
    for maximum speed, washing machine trophy, just drop it.

    - Rule 2 of speedy exit:
    same holds for tank, ammunition, riffle, etc.. etc..
    Mostowski Collapse schrieb am Mittwoch, 14. September 2022 um 18:21:08 UTC+2:
    Biologicians have found a new animal, speedy exit saurus
    aka ruZZian soldier, its the fastest animal on this planet:

    The fastest animals in the world... https://twitter.com/Igor_from_Kyiv_/status/1569758364783054849

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Wed Sep 14 09:25:24 2022
    You can learn a lot from this animal, for example:

    - Rule 1 of speedy exit:
    for maximum speed, washing machine trophy, just drop it.

    - Rule 2 of speedy exit:
    same holds for tank, ammunition, riffle, etc.. etc..

    Mostowski Collapse schrieb am Mittwoch, 14. September 2022 um 18:21:08 UTC+2:
    Biologicians have found a new animal, speedy exit saurus
    aka ruZZian soldier, its the fastest animal on this planet:

    The fastest animals in the world... https://twitter.com/Igor_from_Kyiv_/status/1569758364783054849

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Wed Sep 14 09:21:06 2022
    Biologicians have found a new animal, speedy exit saurus
    aka ruZZian soldier, its the fastest animal on this planet:

    The fastest animals in the world... https://twitter.com/Igor_from_Kyiv_/status/1569758364783054849

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Somebody on Thu Jan 12 05:16:13 2023
    Somebody said:

    I think probabilistic reasoning itself is borken

    Well I was a purist like that also in the past. And I am still a
    kind of purist like that in the present, avoiding probability
    whenever possible. But its a nice little

    mathematical model, which you can map to constraint logic
    programming CLP(R). So if for example you have an
    equation involving probability:

    P(A & B) < P(C)

    Then this says nothing else than the CLP(R) constraint:

    w + z < z + y + x + c

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Thu Jan 12 05:17:16 2023
    Pitty ProbLog doesn’t work like that. How would we name
    this new logic programming language, that can deal with
    probability constraints? Would it be new?

    What about quantum logic programming (QLP)? Would
    possibly need some entanglement equations as well.
    I think there is really the need for the Prolog community

    to do something, there is no logic programming entry here yet:

    Quantum programming languages https://en.wikipedia.org/wiki/Quantum_programming#Quantum_programming_languages

    LoL

    Mostowski Collapse schrieb am Donnerstag, 12. Januar 2023 um 14:16:15 UTC+1:
    Somebody said:

    I think probabilistic reasoning itself is borken

    Well I was a purist like that also in the past. And I am still a
    kind of purist like that in the present, avoiding probability
    whenever possible. But its a nice little

    mathematical model, which you can map to constraint logic
    programming CLP(R). So if for example you have an
    equation involving probability:

    P(A & B) < P(C)

    Then this says nothing else than the CLP(R) constraint:

    w + z < z + y + x + c

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Wed Feb 8 11:25:02 2023
    It is the royal We, as in “We, the Boris of Prolog”

    Yeah, this makes a lot of sense. And ChatGPT is the Agent 007,
    On Her Majesty’s Secret Service. I was thinking of another “we”,
    the “we” from the Dijkstra interview:

    Q: Is the field of computer science approaching maturity in any sense, or where are we?

    A: Well, we is a rather mixed lot aren’t we? https://www.cs.utexas.edu/users/EWD/misc/vanVlissingenInterview.html

    Today I suggrested somebody that somebody should make
    interviews of Jan Wielemaker, Robert Kowalski, etc… I suggested
    some people also working in Philosophy and Logic.

    An interview in the similar vain, but just now at that time of moment,
    although 100 years after the “formal logic” revolution of Boole, Frege, etc…
    but before what OpenAI etc… might bring. Mostlikely

    “formal logic” will have more impact to society than we think now.
    But I don’t have time for that, and I am also not a journalist by profession. Maybe the questions by Boris should make it into such interviews.

    I guess such interviews would be gold in the future. But you see
    I am more into responses from flesh and bone right now. Although
    one could colage some ChatGPT or other bot inverviews into

    such a booklet as well.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Tue Feb 14 01:49:00 2023
    Scryer Prolog isn't that lucky. Their setup_call_cleanup/3
    has some meta predicate issue. And their catch/3 is utterly slow.

    /* Scryer Prolog 0.9.1 */

    ?- time((between(1,500000,_), findall2(X, (X=1;X=2), L), fail; true)).
    % CPU time: 0.000s
    error(existence_error(procedure,'$destroy_findall2_bag'/0),'$destroy_findall2_bag'/0).

    ?- time((between(1,500000,_), findall3(X, (X=1;X=2), L), fail; true)).
    % CPU time: 32.102s
    true.

    Mostowski Collapse schrieb am Dienstag, 14. Februar 2023 um 10:46:02 UTC+1:
    Interesting replacement of setup_call_cleanup/3:

    open(Path, read, Input),
    catch(read_term(Input, Term, Options), Error,
    (close(Input),throw(Error))),
    close(Input) https://github.com/LogtalkDotOrg/logtalk3/blob/master/library/term_io/term_io.lgt

    Can we use this for something?

    Here is some testing, with dry implementation of the bag:

    /* SWI-Prolog 9.1.4 */

    /* N215 Solution */
    ?- time((between(1,500000,_), findall2(X, (X=1;X=2), L), fail; true)).
    % 7,000,000 inferences, 0.875 CPU in 0.871 seconds (100% CPU, 8000000 Lips) true.

    /* Logtalk Idiom */
    ?- time((between(1,500000,_), findall3(X, (X=1;X=2), L), fail; true)).
    % 6,000,000 inferences, 0.500 CPU in 0.497 seconds (101% CPU, 12000000 Lips) true.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Tue Feb 14 01:46:00 2023
    Interesting replacement of setup_call_cleanup/3:

    open(Path, read, Input),
    catch(read_term(Input, Term, Options), Error,
    (close(Input),throw(Error))),
    close(Input) https://github.com/LogtalkDotOrg/logtalk3/blob/master/library/term_io/term_io.lgt

    Can we use this for something?

    Here is some testing, with dry implementation of the bag:

    /* SWI-Prolog 9.1.4 */

    /* N215 Solution */
    ?- time((between(1,500000,_), findall2(X, (X=1;X=2), L), fail; true)).
    % 7,000,000 inferences, 0.875 CPU in 0.871 seconds (100% CPU, 8000000 Lips) true.

    /* Logtalk Idiom */
    ?- time((between(1,500000,_), findall3(X, (X=1;X=2), L), fail; true)).
    % 6,000,000 inferences, 0.500 CPU in 0.497 seconds (101% CPU, 12000000 Lips) true.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Tue Feb 14 02:27:06 2023
    Here is a proposal how to extend the Logtalk idiom by atomicity:

    shield(
    open(Path, read, Input),
    catch(unshield(read_term(Input, Term, Options)), Error,
    (close(Input),throw(Error))),
    close(Input)).

    shield/1 is a new meta predicate inspired by Python:

    awaitable asyncio.shield(aw )
    Protect an awaitable object from being cancelled. https://docs.python.org/3/library/asyncio-task.html#shielding-from-cancellation

    I guess it corresponds to sig_atomic/1 in SWI-Prolog and sys_atomic/1
    in formerly Jekejeke Prolog. unshield/1 reverts shield/1, I didn’t find it yet
    in some existing Prolog system. Disclaimer: The above idea of a

    shielded Logtalk idiom is not yet practically tested.

    Mostowski Collapse schrieb am Dienstag, 14. Februar 2023 um 10:49:01 UTC+1:
    Scryer Prolog isn't that lucky. Their setup_call_cleanup/3
    has some meta predicate issue. And their catch/3 is utterly slow.

    /* Scryer Prolog 0.9.1 */
    ?- time((between(1,500000,_), findall2(X, (X=1;X=2), L), fail; true)).
    % CPU time: 0.000s error(existence_error(procedure,'$destroy_findall2_bag'/0),'$destroy_findall2_bag'/0).
    ?- time((between(1,500000,_), findall3(X, (X=1;X=2), L), fail; true)).
    % CPU time: 32.102s
    true.
    Mostowski Collapse schrieb am Dienstag, 14. Februar 2023 um 10:46:02 UTC+1:
    Interesting replacement of setup_call_cleanup/3:

    open(Path, read, Input),
    catch(read_term(Input, Term, Options), Error, (close(Input),throw(Error))),
    close(Input) https://github.com/LogtalkDotOrg/logtalk3/blob/master/library/term_io/term_io.lgt

    Can we use this for something?

    Here is some testing, with dry implementation of the bag:

    /* SWI-Prolog 9.1.4 */

    /* N215 Solution */
    ?- time((between(1,500000,_), findall2(X, (X=1;X=2), L), fail; true)).
    % 7,000,000 inferences, 0.875 CPU in 0.871 seconds (100% CPU, 8000000 Lips)
    true.

    /* Logtalk Idiom */
    ?- time((between(1,500000,_), findall3(X, (X=1;X=2), L), fail; true)).
    % 6,000,000 inferences, 0.500 CPU in 0.497 seconds (101% CPU, 12000000 Lips)
    true.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Tue Feb 14 05:55:32 2023
    Adding failure handling to it, wouldn’t be extremly difficult,
    but maybe this would slow it down a little bit? Something
    along the following, for the version without shield/1:

    open(Path, read, Input),
    (catch(read_term(Input, Term, Options), Error,
    (close(Input),throw(Error))) -> close(Input)
    ; close(Input))

    Maybe a good name for this less sophisticated setup_call_cleanup/3
    would be simply setup_once_cleanup/3. The once in the name
    would relate to the already existing once/1 predicate and indicate that

    the call is only called once. Which happens for example if the above if-then-else wrapper is used. In the original Logtalk find, the cleanup
    might not be called or multiple times called, since there is no

    if-then-else wrapping. A new meta predicate setup_once_cleanup/3
    could provide a more cleaner solution.

    Mostowski Collapse schrieb am Dienstag, 14. Februar 2023 um 11:27:08 UTC+1:
    Here is a proposal how to extend the Logtalk idiom by atomicity:

    shield(
    open(Path, read, Input),
    catch(unshield(read_term(Input, Term, Options)), Error, (close(Input),throw(Error))),
    close(Input)).

    shield/1 is a new meta predicate inspired by Python:

    awaitable asyncio.shield(aw )
    Protect an awaitable object from being cancelled. https://docs.python.org/3/library/asyncio-task.html#shielding-from-cancellation

    I guess it corresponds to sig_atomic/1 in SWI-Prolog and sys_atomic/1
    in formerly Jekejeke Prolog. unshield/1 reverts shield/1, I didn’t find it yet
    in some existing Prolog system. Disclaimer: The above idea of a

    shielded Logtalk idiom is not yet practically tested.
    Mostowski Collapse schrieb am Dienstag, 14. Februar 2023 um 10:49:01 UTC+1:
    Scryer Prolog isn't that lucky. Their setup_call_cleanup/3
    has some meta predicate issue. And their catch/3 is utterly slow.

    /* Scryer Prolog 0.9.1 */
    ?- time((between(1,500000,_), findall2(X, (X=1;X=2), L), fail; true)).
    % CPU time: 0.000s error(existence_error(procedure,'$destroy_findall2_bag'/0),'$destroy_findall2_bag'/0).
    ?- time((between(1,500000,_), findall3(X, (X=1;X=2), L), fail; true)).
    % CPU time: 32.102s
    true.
    Mostowski Collapse schrieb am Dienstag, 14. Februar 2023 um 10:46:02 UTC+1:
    Interesting replacement of setup_call_cleanup/3:

    open(Path, read, Input),
    catch(read_term(Input, Term, Options), Error, (close(Input),throw(Error))),
    close(Input) https://github.com/LogtalkDotOrg/logtalk3/blob/master/library/term_io/term_io.lgt

    Can we use this for something?

    Here is some testing, with dry implementation of the bag:

    /* SWI-Prolog 9.1.4 */

    /* N215 Solution */
    ?- time((between(1,500000,_), findall2(X, (X=1;X=2), L), fail; true)).
    % 7,000,000 inferences, 0.875 CPU in 0.871 seconds (100% CPU, 8000000 Lips)
    true.

    /* Logtalk Idiom */
    ?- time((between(1,500000,_), findall3(X, (X=1;X=2), L), fail; true)).
    % 6,000,000 inferences, 0.500 CPU in 0.497 seconds (101% CPU, 12000000 Lips)
    true.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Thu Feb 16 13:30:42 2023
    Woa! My new setup_once_cleanup/3, which adopts the Logtalk idiom,
    does something totally different, it overrides the primary exception.
    This is incompatible with the usual setup_call_cleanup/3:

    Logtalk idiom as is:

    ?- once_cleanup(true, throw(foo), throw(bar)).
    Unknown exception: bar

    ?- catch(once_cleanup(true, throw(foo), throw(bar)), E, true).
    E = bar.

    Now compare with what some new Prolog systems do:

    /* Trealla Prolog */
    ?- call_cleanup(throw(foo), throw(bar)).
    throw(foo).

    /* Scryer Prolog */
    ?- call_cleanup(throw(foo), throw(bar)).
    throw(foo).

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Thu Feb 16 15:39:58 2023
    Now I get a little disagreement:

    /* Trealla Prolog */
    ?- call_cleanup(throw(foo), fail).
    false.

    /* Scryer Prolog */
    ?- call_cleanup(throw(foo), fail).
    throw(foo).

    Which one is the desired behaviour?

    Mostowski Collapse schrieb am Donnerstag, 16. Februar 2023 um 22:30:43 UTC+1:
    Woa! My new setup_once_cleanup/3, which adopts the Logtalk idiom,
    does something totally different, it overrides the primary exception.
    This is incompatible with the usual setup_call_cleanup/3:

    Logtalk idiom as is:

    ?- once_cleanup(true, throw(foo), throw(bar)).
    Unknown exception: bar

    ?- catch(once_cleanup(true, throw(foo), throw(bar)), E, true).
    E = bar.

    Now compare with what some new Prolog systems do:

    /* Trealla Prolog */
    ?- call_cleanup(throw(foo), throw(bar)).
    throw(foo).

    /* Scryer Prolog */
    ?- call_cleanup(throw(foo), throw(bar)).
    throw(foo).

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mostowski Collapse on Mon Feb 20 01:30:49 2023
    Exception Chaining:
    I am planning to nevertheless introduce exception chaining,
    adopting some new ideas from Python. In Python a catch of
    a chained exception only matches the head of the chained
    exception. This is an effect of object orientation, since the chain
    is just a field __context__ or something, and the matching is
    based on the class of the exception.

    Maybe can recreate a similar Prolog catch/3, that matches
    either an unchained exception or then the head of chained
    exception. This is medium priority. Python has a further feature
    which could be adopted, the catch/3 handler, if an exception is
    thrown there, it is automatically chained with the current exception.
    This is probably too complicated, no plan to adopt this feature.

    The automatic chaining will probably only be added to
    setup_once_cleanup/3 and not to catch/3. The reason is there is
    some constraint logic programming code that uses catch/3 to
    return a result in branch and bound search. You find this also in
    Markus Triskas code, so making catch/3 too heavy slows down
    the constraint logic programming, unless this code would go
    for the more lower level sys_trap/3.

    Mostowski Collapse schrieb am Montag, 20. Februar 2023 um 10:28:36 UTC+1:
    Now I found two more cases where I could
    use the new setup_once_cleanup/3. These
    correspond to the following in SWI-Prolog:

    with_mutex/2:
    The goal argument is onced. So an implementation
    with setup_call_cleanup/3 is overkill, can be as well
    implemented with setup_once_cleanup/3. I saw that
    with_mutex/2 is implemented natively in SWI-Prolog
    using callProlog, which I guess can be used to create
    a setup_once_cleanup/3 behaviour.

    Pitty the thingy isn’t named once_with_mutex/2. In
    shared lazy tabling I have a strange case for a
    setup_call_cleanup/3 based mutex handling. I guess I
    will rename it to call_with_mutex/2, and also introduce a
    once_with_mutex/2, and see to it that shared eager
    tabling uses the new setup_once_cleanup/3. This is
    a low priority long term change.

    call_with_time_limit/2:
    The goal argument here is onced as well. Pitty the
    thingy isn’t name once_with_time_limit/2. I have a meta
    predicate time_out/2 based on setup_call_cleanup/3 which
    I can now migrate to setup_once_cleanup/3. But maybe I
    will also rename it to once_with_time_limit/2. Oh the horror!
    This is a high priority short term change.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to All on Mon Feb 20 01:28:34 2023
    Now I found two more cases where I could
    use the new setup_once_cleanup/3. These
    correspond to the following in SWI-Prolog:

    with_mutex/2:
    The goal argument is onced. So an implementation
    with setup_call_cleanup/3 is overkill, can be as well
    implemented with setup_once_cleanup/3. I saw that
    with_mutex/2 is implemented natively in SWI-Prolog
    using callProlog, which I guess can be used to create
    a setup_once_cleanup/3 behaviour.

    Pitty the thingy isn’t named once_with_mutex/2. In
    shared lazy tabling I have a strange case for a
    setup_call_cleanup/3 based mutex handling. I guess I
    will rename it to call_with_mutex/2, and also introduce a
    once_with_mutex/2, and see to it that shared eager
    tabling uses the new setup_once_cleanup/3. This is
    a low priority long term change.

    call_with_time_limit/2:
    The goal argument here is onced as well. Pitty the
    thingy isn’t name once_with_time_limit/2. I have a meta
    predicate time_out/2 based on setup_call_cleanup/3 which
    I can now migrate to setup_once_cleanup/3. But maybe I
    will also rename it to once_with_time_limit/2. Oh the horror!
    This is a high priority short term change.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mild Shock@21:1/5 to Mild Shock on Tue Oct 10 16:08:54 2023
    version_data turned out quite useful. I am currently using
    it across Dogelog Player to also return the release date:

    ?- current_prolog_flag(version_data, X).
    X = dogelog(1, 1, 3, [date(1696761013577)]).

    The date is currenty a long integer time stamp. I am not
    using date/3 or datetime/6 compounds for time.

    Mild Shock schrieb am Mittwoch, 11. Oktober 2023 um 00:54:43 UTC+2:
    Is Canada also France? Seems I am not the only one who got
    into struggle with Logtalk sooner or later. LoL

    How its started:
    Ticket raised by me Aug 9, 2021 (when I was "ghost")
    Feature request flag dialect, maybe version and version_data https://github.com/mthom/scryer-prolog/issues/1017

    How its going:
    Commit by pmoura last week
    Delete Scryer Prolog support due to this system refusal to
    support the de facto standard `version_data` flag https://github.com/LogtalkDotOrg/logtalk3/commit/d93883c5a8b014af09bd0e11439eaff30e1c1a5c

    What happened?

    LoL

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mild Shock@21:1/5 to All on Tue Oct 10 15:54:41 2023
    Is Canada also France? Seems I am not the only one who got
    into struggle with Logtalk sooner or later. LoL

    How its started:
    Ticket raised by me Aug 9, 2021 (when I was "ghost")
    Feature request flag dialect, maybe version and version_data https://github.com/mthom/scryer-prolog/issues/1017

    How its going:
    Commit by pmoura last week
    Delete Scryer Prolog support due to this system refusal to
    support the de facto standard `version_data` flag https://github.com/LogtalkDotOrg/logtalk3/commit/d93883c5a8b014af09bd0e11439eaff30e1c1a5c

    What happened?

    LoL

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