France is the Fire Nation of Prolog

[Mostowski Collapse]

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

[Mostowski Collapse]

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]

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]

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]

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

[Mostowski Collapse]

The rustc linter can be used for SAT solving.
https://twitter.com/NieDzejkob/status/1412932919761453058

LoL

[Mostowski Collapse]

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.

[Mostowski Collapse]

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]

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]

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

[Mostowski Collapse]

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]

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]

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.

[Mostowski Collapse]

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]

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]

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]

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]

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]

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]

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.

[Mostowski Collapse]

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]

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

[Mostowski Collapse]

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]

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.

[Mostowski Collapse]

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.

[Mostowski Collapse]

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]

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]

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]

Anyway, these bitrot exchanges are mushrooming,
what about this one, would it be helpful?

https://cs.stackexchange.com/

[Mostowski Collapse]

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]

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

[Mostowski Collapse]

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.

[Mostowski Collapse]

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

[Mostowski Collapse]

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]

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:

[Mostowski Collapse]

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) }

[Julio Di Egidio]

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

[Mostowski Collapse]

LoL, are you feeling tense Culio?

[Mostowski Collapse]

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

[Mostowski Collapse]

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]

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]

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]

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]

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]

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

[Mostowski Collapse]

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]

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]

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]

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

[Mostowski Collapse]

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

[Mostowski Collapse]

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]

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]

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]

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:

[Mostowski Collapse]

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:

[Mostowski Collapse]

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]

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]

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]

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

[Mostowski Collapse]

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]

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]

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

[Mostowski Collapse]

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]

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]

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

[Mostowski Collapse]

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]

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

[Mostowski Collapse]

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

[Mostowski Collapse]

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/

[Mostowski Collapse]

I guess we can overtake Ruby, which is on 19,
if we provide some "Prolog on Rails". Anybody up to it?

[Mostowski Collapse]

(P.S.: The idea would be to provide and base the Rails
functionality in 100% Prolog programming language)

[Mostowski Collapse]

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

[Mostowski Collapse]

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]

Disclaimer: Source of OSTINT, 9gag.com head quarters.
(one should not praise the morning before the evening)

[Mostowski Collapse]

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

[Mostowski Collapse]

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]

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.

[Mostowski Collapse]

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.

[Mostowski Collapse]

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]

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]

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]

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).

[Mostowski Collapse]

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]

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.

[Mostowski Collapse]

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.

[Mild Shock]

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

[Mild Shock]

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.