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

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

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

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

The Kissat SAT solver is a reimplementation of CaDiCaL in C.
https://twitter.com/ArminBiere/status/1288132283443142661

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

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.

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.

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.

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

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

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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

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.

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.