So although it was very temping to download
you software, and then replace these line: <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
By these line:
notation(gliv(X), (~(~X)))
solve_t__sel(neg, C=>X) :-
solve(C=>gliv(X)).
I am afraid I have no time for that. You
could do it by yourself. Or what
On 01/12/2024 15:32, Mild Shock wrote:
So although it was very temping to download
you software, and then replace these line: <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
By these line:
notation(gliv(X), (~(~X)))
solve_t__sel(neg, C=>X) :-
solve(C=>gliv(X)).
Or just change the definition of `dnt`, or create another one. The code
is functional and pretty flexible actually, `notation/5` is `multifile`.
I am afraid I have no time for that. You
could do it by yourself. Or what
I have already done it, and I have already told you the results! You
have no time for anything apparently, except for posting random shit and fucking with thread titles: I have messages all over the place, and it's
just me, you, and Ross once a month...
---
Here is an interesting new case, which I had thought should be
*unsolvable*:
```
?- solve_w([]=>dnt((~(~p)->p)<->p\/(~p))), !. % DNE<->LEM
```
Unsolvable not just because my logic is *affine*, but because the actual statement, provable intuitionistically, is intrinsically higher-order:
```
Theorem DNE_is_LEM : (forall p, ~ ~ p -> p) <-> (forall p, p \/ ~ p).
```
while the statement I am proving above is this one, and it is not intuitionistically provable (AFAICT):
```
Theorem DNE_is_LEM_not_quite : forall p, (~ ~ p -> p) <-> (p \/ ~ p)
```
Yet with my `dnt`, my solver proves even that one (but I still have to inspect the proof tree, what I actually get). Indeed, I am rather
worried that it just solves everything I throw at it, though not the falsities... which is why I am also developing a meta-theory for it, in
Coq:
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-v>
-Julio
And what are the results? Your gist shows
this one here:
% Peirce's law:
solve_case(neg, pierce, [(p->q)->p]=>p).
And you reported:
solve_test::neg:
- pierce: []=>((p->q)->p)->p --> true
solve_test::neg: tot.=1, FAIL=0 --> true.
What do you get with gliv/1?
Julio Di Egidio schrieb:
On 01/12/2024 15:32, Mild Shock wrote:
So although it was very temping to download
you software, and then replace these line:
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11> >> > By these line:
notation(gliv(X), (~(~X)))
solve_t__sel(neg, C=>X) :-
; solve(C=>gliv(X)).
Or just change the definition of `dnt`, or create another one. The
code is functional and pretty flexible actually, `notation/5` is
`multifile`.
I am afraid I have no time for that. You
could do it by yourself. Or what
I have already done it, and I have already told you the results! You
have no time for anything apparently, except for posting random shit
and fucking with thread titles: I have messages all over the place,
and it's just me, you, and Ross once a month...
---
Here is an interesting new case, which I had thought should be
*unsolvable*:
```
?- solve_w([]=>dnt((~(~p)->p)<->p\/(~p))), !. % DNE<->LEM
```
Unsolvable not just because my logic is *affine*, but because the
actual statement, provable intuitionistically, is intrinsically
higher-order:
```
Theorem DNE_is_LEM : (forall p, ~ ~ p -> p) <-> (forall p, p \/ ~ p).
```
while the statement I am proving above is this one, and it is not
intuitionistically provable (AFAICT):
```
Theorem DNE_is_LEM_not_quite : forall p, (~ ~ p -> p) <-> (p \/ ~ p)
```
Yet with my `dnt`, my solver proves even that one (but I still have to
inspect the proof tree, what I actually get). Indeed, I am rather
worried that it just solves everything I throw at it, though not the
falsities... which is why I am also developing a meta-theory for it,
in Coq:
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-v>
-Julio
Hi,
This inference rule is incorrect:
% (C,X->Y=>Z) --> [(C=>X),(C,Y=>Z)]
reduction(elim, imp, (C0=>Z), Gs, Ps) :-
nth1(H, C0, (X->Y), C1),
append(C1, [Y], C2),
Gs = [C1=>X,C2=>Z],
Ps = [H:X,H:Y].
The correct one would be, X->Y has to
be repeated in the left proof branch:
% (C,X->Y=>Z) --> [(C,X->Y=>X),(C,Y=>Z)]
... put your prolog code here ...
Then you can only possibly prove Pierce Law
with Glivenko. Otherwise there is no chance.
See also here:
Mathematical Intuitionism: Introduction to Proof Theory
A. G. Dragalin
§3 THE SEQUENT CALCULUS - Page 11
The calculus GHPC
https://bookstore.ams.org/MMONO/67
Good Luck!
Bye
Mild Shock schrieb:
And what are the results? Your gist shows
this one here:
% Peirce's law:
solve_case(neg, pierce, [(p->q)->p]=>p).
And you reported:
solve_test::neg:
- pierce: []=>((p->q)->p)->p --> true
solve_test::neg: tot.=1, FAIL=0 --> true.
What do you get with gliv/1?
Julio Di Egidio schrieb:
On 01/12/2024 15:32, Mild Shock wrote:
So although it was very temping to download<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
you software, and then replace these line:
;
By these line:
notation(gliv(X), (~(~X)))
solve_t__sel(neg, C=>X) :-
; solve(C=>gliv(X)).
Or just change the definition of `dnt`, or create another one. The
code is functional and pretty flexible actually, `notation/5` is
`multifile`.
I am afraid I have no time for that. You
could do it by yourself. Or what
I have already done it, and I have already told you the results! You
have no time for anything apparently, except for posting random shit
and fucking with thread titles: I have messages all over the place,
and it's just me, you, and Ross once a month...
---
Here is an interesting new case, which I had thought should be
*unsolvable*:
```
?- solve_w([]=>dnt((~(~p)->p)<->p\/(~p))), !. % DNE<->LEM
```
Unsolvable not just because my logic is *affine*, but because the
actual statement, provable intuitionistically, is intrinsically
higher-order:
```
Theorem DNE_is_LEM : (forall p, ~ ~ p -> p) <-> (forall p, p \/ ~ p).
```
while the statement I am proving above is this one, and it is not
intuitionistically provable (AFAICT):
```
Theorem DNE_is_LEM_not_quite : forall p, (~ ~ p -> p) <-> (p \/ ~ p)
```
Yet with my `dnt`, my solver proves even that one (but I still have
to inspect the proof tree, what I actually get). Indeed, I am rather
worried that it just solves everything I throw at it, though not the
falsities... which is why I am also developing a meta-theory for it,
in Coq:
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-v>
-Julio
This inference rule is incorrect:
% (C,X->Y=>Z) --> [(C=>X),(C,Y=>Z)]
reduction(elim, imp, (C0=>Z), Gs, Ps) :-
nth1(H, C0, (X->Y), C1),
append(C1, [Y], C2),
Gs = [C1=>X,C2=>Z],
Ps = [H:X,H:Y].
The correct one would be, X->Y has to
be repeated in the left proof branch:
% (C,X->Y=>Z) --> [(C,X->Y=>X),(C,Y=>Z)]
You see this behaviour here in the graphic
I posted with the answer on proofassistants.stackexchange.com:
Something tells me Glivenko theorem would need at least
intuitionistic logic, to prove for example Peirce law (*): https://i.sstatic.net/lGQ8Iur9.png
The (L->) rule is applied twice, to prove
Pierce Law via Glivenko. You can only apply (L->)
twice if you implement Dragalins variant that
keeps X->Y in the right branch of then (L->) rule.
If you don't implement Dragalins implication, i.e.
if you don't implement intuitistic implication in
your Prolog code, I guess there is no chance for
Glivenkos theorem. You will be pretty much on your
own in a totally different terrain.
Mild Shock schrieb:
Hi,
This inference rule is incorrect:
% (C,X->Y=>Z) --> [(C=>X),(C,Y=>Z)]
reduction(elim, imp, (C0=>Z), Gs, Ps) :-
nth1(H, C0, (X->Y), C1),
append(C1, [Y], C2),
Gs = [C1=>X,C2=>Z],
Ps = [H:X,H:Y].
The correct one would be, X->Y has to
be repeated in the left proof branch:
% (C,X->Y=>Z) --> [(C,X->Y=>X),(C,Y=>Z)]
... put your prolog code here ...
Then you can only possibly prove Pierce Law
with Glivenko. Otherwise there is no chance.
See also here:
Mathematical Intuitionism: Introduction to Proof Theory
A. G. Dragalin
§3 THE SEQUENT CALCULUS - Page 11
The calculus GHPC
https://bookstore.ams.org/MMONO/67
Good Luck!
Bye
Mild Shock schrieb:
And what are the results? Your gist shows
this one here:
% Peirce's law:
solve_case(neg, pierce, [(p->q)->p]=>p).
And you reported:
solve_test::neg:
- pierce: []=>((p->q)->p)->p --> true
solve_test::neg: tot.=1, FAIL=0 --> true.
What do you get with gliv/1?
Julio Di Egidio schrieb:
On 01/12/2024 15:32, Mild Shock wrote:
So although it was very temping to download<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11> >>>> > By these line:
you software, and then replace these line:
;
notation(gliv(X), (~(~X)))
solve_t__sel(neg, C=>X) :-
; solve(C=>gliv(X)).
Or just change the definition of `dnt`, or create another one. The
code is functional and pretty flexible actually, `notation/5` is
`multifile`.
I am afraid I have no time for that. You
could do it by yourself. Or what
I have already done it, and I have already told you the results!
You have no time for anything apparently, except for posting random
shit and fucking with thread titles: I have messages all over the
place, and it's just me, you, and Ross once a month...
---
Here is an interesting new case, which I had thought should be
*unsolvable*:
```
?- solve_w([]=>dnt((~(~p)->p)<->p\/(~p))), !. % DNE<->LEM
```
Unsolvable not just because my logic is *affine*, but because the
actual statement, provable intuitionistically, is intrinsically
higher-order:
```
Theorem DNE_is_LEM : (forall p, ~ ~ p -> p) <-> (forall p, p \/ ~ p).
```
while the statement I am proving above is this one, and it is not
intuitionistically provable (AFAICT):
```
Theorem DNE_is_LEM_not_quite : forall p, (~ ~ p -> p) <-> (p \/ ~ p)
```
Yet with my `dnt`, my solver proves even that one (but I still have
to inspect the proof tree, what I actually get). Indeed, I am
rather worried that it just solves everything I throw at it, though
not the falsities... which is why I am also developing a meta-theory
for it, in Coq:
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-v>
-Julio
On 01/12/2024 16:50, Mild Shock wrote:
This inference rule is incorrect:
% (C,X->Y=>Z) --> [(C=>X),(C,Y=>Z)]
reduction(elim, imp, (C0=>Z), Gs, Ps) :-
nth1(H, C0, (X->Y), C1),
append(C1, [Y], C2),
Gs = [C1=>X,C2=>Z],
Ps = [H:X,H:Y].
The correct one would be, X->Y has to
be repeated in the left proof branch:
% (C,X->Y=>Z) --> [(C,X->Y=>X),(C,Y=>Z)]
You are incorrect: that the logic is *affine* indeed means that we
cannot use hypotheses more than once.
This is a nice intro scheme, notice also that this is all quite
orthogonal to the classical vs intuitionistic distinction:
<https://en.wikipedia.org/wiki/Substructural_type_system>
HTH.
-Julio
Well then Pierce Law is not povable under
the usual Glivenko translation in affine logic.
So what? Whats your point?
I found only one book that discusses Glivenk
style translations for substructural logics:
Chatpter 8: Glivenko Theorems
Residuated Lattices: an algebraic glimpse at substructural logics https://www.researchgate.net/publication/235626321
But how do you prove rigorously that affine
logic rejects certain Glivenko translations.
You would need to have a (counter-)model finder and
not a proof finder. The "algebraic viewpoint"
could help you in building a (counter-)model finder.
What also sometimes helps is to use modal
translations together with (counter-)model finders,
that would then search for some tree models.
Julio Di Egidio schrieb:
On 01/12/2024 16:50, Mild Shock wrote:
This inference rule is incorrect:
% (C,X->Y=>Z) --> [(C=>X),(C,Y=>Z)]
reduction(elim, imp, (C0=>Z), Gs, Ps) :-
nth1(H, C0, (X->Y), C1),
append(C1, [Y], C2),
Gs = [C1=>X,C2=>Z],
Ps = [H:X,H:Y].
The correct one would be, X->Y has to
be repeated in the left proof branch:
% (C,X->Y=>Z) --> [(C,X->Y=>X),(C,Y=>Z)]
You are incorrect: that the logic is *affine* indeed means that we
cannot use hypotheses more than once.
This is a nice intro scheme, notice also that this is all quite
orthogonal to the classical vs intuitionistic distinction:
<https://en.wikipedia.org/wiki/Substructural_type_system>
HTH.
-Julio
Hi,
Linear logic you can of course do the following,
and define intuitionistic implication as follows:
A -> B := ! A -o B
Girards Exponention will do the repeating for you,
that is found in Dragalins Implication.
I don't know how to incorporate the same into your Prolog code.
Bye
Mild Shock schrieb:
You see this behaviour here in the graphic
I posted with the answer on proofassistants.stackexchange.com:
Something tells me Glivenko theorem would need at least
intuitionistic logic, to prove for example Peirce law (*):
https://i.sstatic.net/lGQ8Iur9.png
The (L->) rule is applied twice, to prove
Pierce Law via Glivenko. You can only apply (L->)
twice if you implement Dragalins variant that
keeps X->Y in the right branch of then (L->) rule.
If you don't implement Dragalins implication, i.e.
if you don't implement intuitistic implication in
your Prolog code, I guess there is no chance for
Glivenkos theorem. You will be pretty much on your
own in a totally different terrain.
Mild Shock schrieb:
Hi,
This inference rule is incorrect:
% (C,X->Y=>Z) --> [(C=>X),(C,Y=>Z)]
reduction(elim, imp, (C0=>Z), Gs, Ps) :-
nth1(H, C0, (X->Y), C1),
append(C1, [Y], C2),
Gs = [C1=>X,C2=>Z],
Ps = [H:X,H:Y].
The correct one would be, X->Y has to
be repeated in the left proof branch:
% (C,X->Y=>Z) --> [(C,X->Y=>X),(C,Y=>Z)]
... put your prolog code here ...
Then you can only possibly prove Pierce Law
with Glivenko. Otherwise there is no chance.
See also here:
Mathematical Intuitionism: Introduction to Proof Theory
A. G. Dragalin
§3 THE SEQUENT CALCULUS - Page 11
The calculus GHPC
https://bookstore.ams.org/MMONO/67
Good Luck!
Bye
Mild Shock schrieb:
And what are the results? Your gist shows
this one here:
% Peirce's law:
solve_case(neg, pierce, [(p->q)->p]=>p).
And you reported:
solve_test::neg:
- pierce: []=>((p->q)->p)->p --> true
solve_test::neg: tot.=1, FAIL=0 --> true.
What do you get with gliv/1?
Julio Di Egidio schrieb:
On 01/12/2024 15:32, Mild Shock wrote:
So although it was very temping to download<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11> >>>>> > By these line:
you software, and then replace these line:
;
notation(gliv(X), (~(~X)))
solve_t__sel(neg, C=>X) :-
; solve(C=>gliv(X)).
Or just change the definition of `dnt`, or create another one. The >>>>> code is functional and pretty flexible actually, `notation/5` is
`multifile`.
I am afraid I have no time for that. You
could do it by yourself. Or what
I have already done it, and I have already told you the results!
You have no time for anything apparently, except for posting random
shit and fucking with thread titles: I have messages all over the
place, and it's just me, you, and Ross once a month...
---
Here is an interesting new case, which I had thought should be
*unsolvable*:
```
?- solve_w([]=>dnt((~(~p)->p)<->p\/(~p))), !. % DNE<->LEM
```
Unsolvable not just because my logic is *affine*, but because the
actual statement, provable intuitionistically, is intrinsically
higher-order:
```
Theorem DNE_is_LEM : (forall p, ~ ~ p -> p) <-> (forall p, p \/ ~ p). >>>>> ```
while the statement I am proving above is this one, and it is not
intuitionistically provable (AFAICT):
```
Theorem DNE_is_LEM_not_quite : forall p, (~ ~ p -> p) <-> (p \/ ~ p) >>>>> ```
Yet with my `dnt`, my solver proves even that one (but I still have
to inspect the proof tree, what I actually get). Indeed, I am
rather worried that it just solves everything I throw at it, though
not the falsities... which is why I am also developing a
meta-theory for it, in Coq:
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-v>
-Julio
Well then Pierce Law is not povable under
the usual Glivenko translation in affine logic.
So what? Whats your point?
I found only one book that discusses Glivenk
style translations for substructural logics:
Chatpter 8: Glivenko Theorems
Residuated Lattices: an algebraic glimpse at substructural logics https://www.researchgate.net/publication/235626321
On 01/12/2024 17:27, Mild Shock wrote:
Well then Pierce Law is not povable under
the usual Glivenko translation in affine logic.
So what? Whats your point?
That my TNT (I am now dubbing it "triple-negation translation") instead works, and where is some piece of theory to attach to it?
I found only one book that discusses Glivenk
style translations for substructural logics:
Chatpter 8: Glivenko Theorems
Residuated Lattices: an algebraic glimpse at substructural logics
https://www.researchgate.net/publication/235626321
Indeed there is a lot of not much around. But Girard talks about not
having and not wanting a separate semantics, it's all purely syntactic.
But I still have only a vague intuition about what that means. <https://girard.perso.math.cnrs.fr/0.pdf>
Anyway, pretty much along that line, I am thinking: could I prove in
Prolog the meta-properties I have proved in Coq (so far)?
Meta-programming and program-analysis features of Prolog are certainly
not lacking...
-Julio
Ok my fault I tested Glivenko and not your TNT,
with TNT I get indeed this here:
?- solve_case(TT, pierce, G), solve_t__sel(TT, G).
TT = neg,
G = ([((p->q)->p)]=>p).
Oki Doki
But I am not familiar with this proof display:
[
impI((p->0))
impI((p->0))
[
impE1(1:(p->q))
impI(p)
[
impE1(1:p)
unif(2:p)
]
[
impE2(1:0)
botE(3:0)
]
]
[
impE2(1:p)
[
impE1(1:p)
unif(2:p)
]
[
impE2(1:0)
unif(3:0)
]
]
]
How is one supposed to read the above?
On 01/12/2024 15:32, Mild Shock wrote:
So although it was very temping to download
you software, and then replace these line: <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
By these line:
notation(gliv(X), (~(~X)))
solve_t__sel(neg, C=>X) :-
solve(C=>gliv(X)).
Or just change the definition of `dnt`, or create another one. The code
is functional and pretty flexible actually, `notation/5` is `multifile`.
I am afraid I have no time for that. You
could do it by yourself. Or what
I have already done it, and I have already told you the results! You
have no time for anything apparently, except for posting random shit and fucking with thread titles: I have messages all over the place, and it's
just me, you, and Ross once a month...
---
Here is an interesting new case, which I had thought should be
*unsolvable*:
```
?- solve_w([]=>dnt((~(~p)->p)<->p\/(~p))), !. % DNE<->LEM
```
Unsolvable not just because my logic is *affine*, but because the actual statement, provable intuitionistically, is intrinsically higher-order:
```
Theorem DNE_is_LEM : (forall p, ~ ~ p -> p) <-> (forall p, p \/ ~ p).
```
while the statement I am proving above is this one, and it is not intuitionistically provable (AFAICT):
```
Theorem DNE_is_LEM_not_quite : forall p, (~ ~ p -> p) <-> (p \/ ~ p)
```
Yet with my `dnt`, my solver proves even that one (but I still have to inspect the proof tree, what I actually get). Indeed, I am rather
worried that it just solves everything I throw at it, though not the falsities... which is why I am also developing a meta-theory for it, in
Coq:
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-v>
-Julio
It didn't work, I was running:
?- solve_case(TT, pierce, G), solve_t__sel(TT, G).
And it showed me in SWI-Prolog false:
false.
But the result shoud be true.
Julio Di Egidio schrieb:
On 01/12/2024 17:27, Mild Shock wrote:
Well then Pierce Law is not povable under
the usual Glivenko translation in affine logic.
So what? Whats your point?
That my TNT (I am now dubbing it "triple-negation translation")
instead works, and where is some piece of theory to attach to it?
I found only one book that discusses Glivenk
style translations for substructural logics:
Chatpter 8: Glivenko Theorems
Residuated Lattices: an algebraic glimpse at substructural logics
https://www.researchgate.net/publication/235626321
Indeed there is a lot of not much around. But Girard talks about not
having and not wanting a separate semantics, it's all purely
syntactic. But I still have only a vague intuition about what that means.
<https://girard.perso.math.cnrs.fr/0.pdf>
Anyway, pretty much along that line, I am thinking: could I prove in
Prolog the meta-properties I have proved in Coq (so far)?
Meta-programming and program-analysis features of Prolog are certainly
not lacking...
-Julio
Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
?- solve_case(TT, pelletier, G), time(solve_t__sel(TT, G)).
Action (h for help) ? abort
% 844,501,974 inferences, 63.891 CPU in 68.236 seconds (94% CPU,
13217933 Lips)
% Execution Aborted
The test case was:
solve_case(neg, pelletier, []=>((p<->(q<->r))<->(p<->q))).
Or just a problem of explosion?
Julio Di Egidio schrieb:
On 01/12/2024 15:32, Mild Shock wrote:
So although it was very temping to download
you software, and then replace these line:
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11> >> > By these line:
notation(gliv(X), (~(~X)))
solve_t__sel(neg, C=>X) :-
; solve(C=>gliv(X)).
Or just change the definition of `dnt`, or create another one. The
code is functional and pretty flexible actually, `notation/5` is
`multifile`.
I am afraid I have no time for that. You
could do it by yourself. Or what
I have already done it, and I have already told you the results! You
have no time for anything apparently, except for posting random shit
and fucking with thread titles: I have messages all over the place,
and it's just me, you, and Ross once a month...
---
Here is an interesting new case, which I had thought should be
*unsolvable*:
```
?- solve_w([]=>dnt((~(~p)->p)<->p\/(~p))), !. % DNE<->LEM
```
Unsolvable not just because my logic is *affine*, but because the
actual statement, provable intuitionistically, is intrinsically
higher-order:
```
Theorem DNE_is_LEM : (forall p, ~ ~ p -> p) <-> (forall p, p \/ ~ p).
```
while the statement I am proving above is this one, and it is not
intuitionistically provable (AFAICT):
```
Theorem DNE_is_LEM_not_quite : forall p, (~ ~ p -> p) <-> (p \/ ~ p)
```
Yet with my `dnt`, my solver proves even that one (but I still have to
inspect the proof tree, what I actually get). Indeed, I am rather
worried that it just solves everything I throw at it, though not the
falsities... which is why I am also developing a meta-theory for it,
in Coq:
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-v>
-Julio
Similar problem here:
?- solve_case(TT, pelletier2, G), time(solve_t__sel(TT, G)).
Action (h for help) ? abort
% 1,368,141,792 inferences, 103.188 CPU in 109.107 seconds (95% CPU,
13258794 Lips)
% Execution Aborted
Mostlikely the reduction has way too much backtracking,
the implementation of some Gentzen inversion lemmas
is lacking. Gentzen inversion lemma allow to place
cuts in the proof search. I don't know how you formulate
this in Coq. I even don't know whether your Coq formalization
models the Prolog non-determinism.
The test case was:
solve_case(pos, pelletier2, []=>((p<->(q<->(r<->s)))<->(p<->(q<->r)))).
Mild Shock schrieb:
Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
?- solve_case(TT, pelletier, G), time(solve_t__sel(TT, G)).
Action (h for help) ? abort
% 844,501,974 inferences, 63.891 CPU in 68.236 seconds (94% CPU,
13217933 Lips)
% Execution Aborted
The test case was:
solve_case(neg, pelletier, []=>((p<->(q<->r))<->(p<->q))).
Or just a problem of explosion?
Julio Di Egidio schrieb:
On 01/12/2024 15:32, Mild Shock wrote:
So although it was very temping to download<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
you software, and then replace these line:
;
By these line:
notation(gliv(X), (~(~X)))
solve_t__sel(neg, C=>X) :-
; solve(C=>gliv(X)).
Or just change the definition of `dnt`, or create another one. The
code is functional and pretty flexible actually, `notation/5` is
`multifile`.
I am afraid I have no time for that. You
could do it by yourself. Or what
I have already done it, and I have already told you the results! You
have no time for anything apparently, except for posting random shit
and fucking with thread titles: I have messages all over the place,
and it's just me, you, and Ross once a month...
---
Here is an interesting new case, which I had thought should be
*unsolvable*:
```
?- solve_w([]=>dnt((~(~p)->p)<->p\/(~p))), !. % DNE<->LEM
```
Unsolvable not just because my logic is *affine*, but because the
actual statement, provable intuitionistically, is intrinsically
higher-order:
```
Theorem DNE_is_LEM : (forall p, ~ ~ p -> p) <-> (forall p, p \/ ~ p).
```
while the statement I am proving above is this one, and it is not
intuitionistically provable (AFAICT):
```
Theorem DNE_is_LEM_not_quite : forall p, (~ ~ p -> p) <-> (p \/ ~ p)
```
Yet with my `dnt`, my solver proves even that one (but I still have
to inspect the proof tree, what I actually get). Indeed, I am rather
worried that it just solves everything I throw at it, though not the
falsities... which is why I am also developing a meta-theory for it,
in Coq:
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-v>
-Julio
Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
?- solve_case(TT, pelletier, G), time(solve_t__sel(TT, G)).
solve_case(neg, pelletier, []=>((p<->(q<->r))<->(p<->q))).
Or just a problem of explosion?
?- unfold(tnt((p<->(q<->r))<->(p<->q)), Qs).
How does one usually demonstrate
Glivenkos theorem?
Its actually easier, you don't need to go
semantical. You need only to show that
Consequentia mirabilis aka Calvius Law
becomes admissible as an inference rule:
G, ~A |- A
---------------- (MIR)
G |- A
https://de.wikipedia.org/wiki/Consequentia_mirabilis
Which is a form of contraction. See also
Lectures on the Curry-Howard Isomorphism
6.6 The pure impicational fragment https://shop.elsevier.com/books/lectures-on-the-curry-howard-isomorphism/sorensen/978-0-444-52077-7
The reason is that if you add MIR to
intuitionistic logic you get classical logic.
MIR is a very funny inference rule,
when you show it as an axiom schema:
((A -> f) -> A) -> A
Its a specialization of Peirce Law.
((P -> Q) -> P) -> P
Just set Q = f.
Julio Di Egidio schrieb:
On 02/12/2024 09:31, Mild Shock wrote:
How does one usually demonstrate
Glivenkos theorem?
Usually with a semantics: we have already said that up-thread...
-Julio
On 02/12/2024 09:31, Mild Shock wrote:
How does one usually demonstrate
Glivenkos theorem?
Usually with a semantics: we have already said that up-thread...
-Julio
) is invertible, (L->) is not invertible.Invertible rules such as (R->) can be greedily
On 02/12/2024 12:37, Julio Di Egidio wrote:
?- unfold(tnt((p<->(q<->r))<->(p<->q)), Qs).
(That should have been an `X`, not a `Qs`, that is a formula, not a
proof tree: anyway, you get the point.)
-Julio
Glivenko is a basically RAA, reductio ad
absurdum shifted to the root. This is another
way to proof Glivenkos theorem.
I highly confused Joseph Vidal-Rosset on
SWI-Prolog discourse when I showed him
a intuitionistic prover that sometimes
also includes RAA, and then produces a classical
proof. RAA, reductio ad absurdum is this
inference rule:
G, ~A |- f
------------- (RAA)
G |- A
Compare this to Glivenko, basically double
negation elimiantion at the root:
???
---------------
G |- ~(~A)
--------------- (GLI)
G |- A
But what happens above G |- ~(~A), i.e. the
???? . By Gentzen inversion lemma, above
G |- ~(~A) we must find, G, ~A |- f,
and we are back to RAA:
G, ~A |- f
--------------- (R->) Gentzen inversion lemma
G |- ~(~A)
--------------- (GLI)
G |- A
So as much as Glivenko appears as a new alien
ivention, it has much to do with they age old
idea of "indirect proof".
Mild Shock schrieb:
Its actually easier, you don't need to go
semantical. You need only to show that
Consequentia mirabilis aka Calvius Law
becomes admissible as an inference rule:
G, ~A |- A
---------------- (MIR)
G |- A
https://de.wikipedia.org/wiki/Consequentia_mirabilis
Which is a form of contraction. See also
Lectures on the Curry-Howard Isomorphism
6.6 The pure impicational fragment
https://shop.elsevier.com/books/lectures-on-the-curry-howard-isomorphism/sorensen/978-0-444-52077-7
The reason is that if you add MIR to
intuitionistic logic you get classical logic.
MIR is a very funny inference rule,
when you show it as an axiom schema:
((A -> f) -> A) -> A
Its a specialization of Peirce Law.
((P -> Q) -> P) -> P
Just set Q = f.
Julio Di Egidio schrieb:
On 02/12/2024 09:31, Mild Shock wrote:
How does one usually demonstrate
Glivenkos theorem?
Usually with a semantics: we have already said that up-thread...
-Julio
Here is an interesting new case, which I had thought should be<snip>
*unsolvable*:
```
?- solve_w([]=>dnt((~(~p)->p)<->p\/(~p))), !. % DNE<->LEM
```
Yet with my `dnt`, my solver proves even that one (but I still have to inspect the proof tree, what I actually get). Indeed, I am rather
worried that it just solves everything I throw at it, though not the falsities...
Its actually easier, you don't need to go
semantical. You need only to show that
Consequentia mirabilis aka Calvius Law
becomes admissible as an inference rule:
G, ~A |- A
---------------- (MIR)
G |- A
https://de.wikipedia.org/wiki/Consequentia_mirabilis
Which is a form of contraction.
On 01/12/2024 15:32, Mild Shock wrote:
I am afraid I have no time for that. You
could do it by yourself. Or what
I have already done it, and I have already told you the results! You
have no time for anything apparently, except for posting random shit and fucking with thread titles: I have messages all over the place, and it's
just me, you, and Ross once a month...
Which is a form of contraction.
Which is not allowed in a linear or affine logic.
Also, with reference to another comment of yours: my rules are
"directed", and that is a feature... as I have read somewhere.
On 01/12/2024 15:32, Mild Shock wrote:
So although it was very temping to download
you software, and then replace these line: <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
By these line:
notation(gliv(X), (~(~X)))
solve_t__sel(neg, C=>X) :-
solve(C=>gliv(X)).
Or just change the definition of `dnt`, or create another one. The code
is functional and pretty flexible actually, `notation/5` is `multifile`.
I am afraid I have no time for that. You
could do it by yourself. Or what
I have already done it, and I have already told you the results! You
have no time for anything apparently, except for posting random shit and fucking with thread titles: I have messages all over the place, and it's
just me, you, and Ross once a month...
---
Here is an interesting new case, which I had thought should be
*unsolvable*:
```
?- solve_w([]=>dnt((~(~p)->p)<->p\/(~p))), !. % DNE<->LEM
```
Unsolvable not just because my logic is *affine*, but because the actual statement, provable intuitionistically, is intrinsically higher-order:
```
Theorem DNE_is_LEM : (forall p, ~ ~ p -> p) <-> (forall p, p \/ ~ p).
```
while the statement I am proving above is this one, and it is not intuitionistically provable (AFAICT):
```
Theorem DNE_is_LEM_not_quite : forall p, (~ ~ p -> p) <-> (p \/ ~ p)
```
Yet with my `dnt`, my solver proves even that one (but I still have to inspect the proof tree, what I actually get). Indeed, I am rather
worried that it just solves everything I throw at it, though not the falsities... which is why I am also developing a meta-theory for it, in
Coq:
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-v>
-Julio
Now I tried an example by Troelstra & Schwichtenberg:
solve_case(pos, schwichtenberg, [((((p->q)->q)->p)->q),(q->p)]=>q). solve_case(neg, schwichtenberg2, [((((p->q)->q)->p)->q),(q->p)]=>q).
At least the second case shouldn't give false, as is seen here:
On 02/12/2024 09:49, Mild Shock wrote:.
Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
The solver *is* very slow at the moment, and you are trying to prove a
too complicated statement:
```
?- unfold(tnt((p<->(q<->r))<->(p<->q)), Qs).
Qs = ((((p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p)->(p->q)/\(q->p))/\((p->q)/\(q->p)->(p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p))->0)->(((p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p)->(p->q)/\(q->p))/\((p->q)/\(q->p)->(p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p))->0)->0)
```
On 02/12/2024 12:37, Julio Di Egidio wrote:0).
On 02/12/2024 09:49, Mild Shock wrote:
Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
The solver *is* very slow at the moment, and you are trying to prove a
too complicated statement:
```
?- unfold(tnt((p<->(q<->r))<->(p<->q)), Qs).
Qs =
((((p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p)->(p->q)/\(q->p))/\((p->q)/\(q->p)->(p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p))->0)->(((p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p)->(p->q)/\(q->p))/\((p->q)/\(q->p)->(p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p))->0)->
```
Yeah, there is definitely a bug, though unrelated to TNT: the reduction
rules are applied in the order of definition, and I can confirm that, depending on that order, the solver may not terminate.
Would you think there is an order that works? Otherwise it gets complicated...
On 05/12/2024 22:26, Julio Di Egidio wrote:0).
On 02/12/2024 12:37, Julio Di Egidio wrote:
On 02/12/2024 09:49, Mild Shock wrote:
Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
The solver *is* very slow at the moment, and you are trying to prove
a too complicated statement:
```
?- unfold(tnt((p<->(q<->r))<->(p<->q)), Qs).
Qs =
((((p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p)->(p->q)/\(q->p))/\((p->q)/\(q->p)->(p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p))->0)->(((p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p)->(p->q)/\(q->p))/\((p->q)/\(q->p)->(p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p))->0)->
```
Yeah, there is definitely a bug, though unrelated to TNT: the
reduction rules are applied in the order of definition, and I can
confirm that, depending on that order, the solver may not terminate.
Would you think there is an order that works? Otherwise it gets
complicated...
It's slowly dawning on me what might be going wrong: I have proved that reductions decrease the goal size *for each residual goal*, but each reduction may produce more than one residual goal, and I have not proved
that the proof search will not keep branching indefinitely...
-Julio
Yes, a binary tree of depth n, can still have 2^n nodes.
Unless you apply some pruning technique.
The typical pruning technique in proof search is
Gentzens inversion lemma.
Julio Di Egidio schrieb:
On 05/12/2024 22:26, Julio Di Egidio wrote:0).
On 02/12/2024 12:37, Julio Di Egidio wrote:
On 02/12/2024 09:49, Mild Shock wrote:
Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
The solver *is* very slow at the moment, and you are trying to prove
a too complicated statement:
```
?- unfold(tnt((p<->(q<->r))<->(p<->q)), Qs).
Qs =
((((p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p)->(p->q)/\(q->p))/\((p->q)/\(q->p)->(p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p))->0)->(((p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p)->(p->q)/\(q->p))/\((p->q)/\(q->p)->(p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p))->0)-
```
Yeah, there is definitely a bug, though unrelated to TNT: the
reduction rules are applied in the order of definition, and I can
confirm that, depending on that order, the solver may not terminate.
Would you think there is an order that works? Otherwise it gets
complicated...
It's slowly dawning on me what might be going wrong: I have proved
that reductions decrease the goal size *for each residual goal*, but
each reduction may produce more than one residual goal, and I have not
proved that the proof search will not keep branching indefinitely...
-Julio
On 06/12/2024 16:58, Mild Shock wrote:
Cut away certain rules, avoiding even more backtracking.
I had `once` initially, as that certainly makes sense, but it was
failing even some of the simpler pos cases. I shall try again.
So basically you would replace something like:
nth1(N, List, Lit, List2)
select(Lit, List, List2)
member(Lit, List)
By this here:
once(nth1(N, List, Lit, List2))
once(select(Lit, List, List2))
once(member(Lit, List))
No need to backtrack over multiple literals.
With Gentzen inversion lemmas you can even go a step farther:
nth1(N, List, Lit, List2), !
select(Lit, List, List2), !
member(Lit, List), !
Cut away certain rules, avoiding even more backtracking.
Hi,
Or start with a deterministic system,
and show that it is immune to how the problem
is stated, immune to all the structural rules.
For example this deterministic classical prover,
for propositional logic. It gives an example
what I mean by Gentzen inversion lemmas:
prove(L) :- select((A->B),L,R), !, prove([-A,B|R]).
prove(L) :- select(-(A->B),L,R), !, prove([A|R]), prove([-B|R]).
prove(L) :- select(-A,L,R), member(A,R), !.
The cut (!)/0 in the first and second claus is justified
by Gentzen inversion lemmas found here, check out page 81:
Basic Proof Theory, Cambridge University Press
A. S. Troelstra & H. Schwichtenberg - June 2012 https://www.cambridge.org/core/books/basic-proof-theory/928508F797214A017D245A1FB67CCCD9
It can readily prove Peirce Law:
?- prove([(((p->q)->p)->p)]).
true.
But with Coq or Isabelle/HOL you should be
also able to prove these meta theorems about
the Prolog predicate prove/1:
prove([...,X,Y,...])
----------------------- (Exchange)
prove([...,X,Y,...])
prove([...,X,X,...])
----------------------- (Contraction)
prove([...,X,...])
prove([...,X,...])
----------------------- (Weakening)
prove([...,Y,X,...])
https://en.wikipedia.org/wiki/Structural_rule
Bye
Julio Di Egidio schrieb:
On 06/12/2024 17:17, Julio Di Egidio wrote:
On 06/12/2024 16:58, Mild Shock wrote:
Cut away certain rules, avoiding even more backtracking.
I had `once` initially, as that certainly makes sense, but it was
failing even some of the simpler pos cases. I shall try again.
Indeed, not even a plain `once` works since there may be more than one
*different* matching hypothesis, and committing to the first one in
order may lead to failure.
Anyway, as said, I'd rather not cut on the search space (at all), plus
I don't see how cutting should matter to termination (given that the
reduction rules are not recursive).
I need to think more about it: what is exactly going wrong.
-Julio
On 06/12/2024 17:17, Julio Di Egidio wrote:
On 06/12/2024 16:58, Mild Shock wrote:
Cut away certain rules, avoiding even more backtracking.
I had `once` initially, as that certainly makes sense, but it was
failing even some of the simpler pos cases. I shall try again.
Indeed, not even a plain `once` works since there may be more than one *different* matching hypothesis, and committing to the first one in
order may lead to failure.
Anyway, as said, I'd rather not cut on the search space (at all), plus I don't see how cutting should matter to termination (given that the
reduction rules are not recursive).
I need to think more about it: what is exactly going wrong.
-Julio
On 04/12/2024 08:47, Mild Shock wrote:
Now I tried an example by Troelstra & Schwichtenberg:
solve_case(pos, schwichtenberg, [((((p->q)->q)->p)->q),(q->p)]=>q).
solve_case(neg, schwichtenberg2, [((((p->q)->q)->p)->q),(q->p)]=>q).
At least the second case shouldn't give false, as is seen here:
It fails if you do (the equivalent of) the intros before the TNT: I had
a doubt about that, thanks for the test case. This works as expected:
?- solve([]=>tnt((((((p->q)->q)->p)->q)/\(q->p))->q)).
-Julio
Ok, this here is classical logic,
deterministically expressed:
prove(L) :- select((A->B),L,R), !, prove([-A,B|R]).
prove(L) :- select(-(A->B),L,R), !, prove([A|R]), prove([-B|R]).
prove(L) :- select(-A,L,R), member(A,R), !.
It can readily prove Peirce Law:
?- prove([(((p->q)->p)->p)]).
true.
With Coq or Isabelle/HOL you should be
also able to prove these meta theorems about
the Prolog predicate prove/1:
prove([...,X,Y,...])
----------------------- (Exchange)
prove([...,Y,X,...])
prove([...,X,X,...])
----------------------- (Contraction)
prove([...,X,...])
prove([...,X,...])
----------------------- (Weakening)
prove([...,Y,X,...])
https://en.wikipedia.org/wiki/Structural_rule
If you replace prove/1 with a deterministic prover
for affine logic, I guess you will still be
able to verify (Exchange) and (Weakening) for
an arbitary input. But not anymore (Contraction)
in general. What is the deterministic prover for
affine logic?
Julio Di Egidio schrieb:
On 04/12/2024 08:47, Mild Shock wrote:
Now I tried an example by Troelstra & Schwichtenberg:
solve_case(pos, schwichtenberg, [((((p->q)->q)->p)->q),(q->p)]=>q).
solve_case(neg, schwichtenberg2, [((((p->q)->q)->p)->q),(q->p)]=>q).
At least the second case shouldn't give false, as is seen here:
It fails if you do (the equivalent of) the intros before the TNT: I
had a doubt about that, thanks for the test case. This works as
expected:
?- solve([]=>tnt((((((p->q)->q)->p)->q)/\(q->p))->q)).
-Julio
On 02/12/2024 12:37, Julio Di Egidio wrote:
On 02/12/2024 09:49, Mild Shock wrote:
Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
The solver *is* very slow at the moment, and you are trying to prove a
too complicated statement:
```
?- unfold(tnt((p<->(q<->r))<->(p<->q)), X).
```
On 05/12/2024 22:26, Julio Di Egidio wrote:
On 02/12/2024 12:37, Julio Di Egidio wrote:
On 02/12/2024 09:49, Mild Shock wrote:
Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
The solver *is* very slow at the moment, and you are trying to prove
a too complicated statement:
```
?- unfold(tnt((p<->(q<->r))<->(p<->q)), X).
```
That 'pelletier' is actually false. I guess you have miscopied it, this
one is true (classically):
`((p <-> (q <-> r)) <-> (p <-> q)) <-> r`.
Meanwhile, I have narrowed the problem of non-termination down to the imp-elim rule, and already have a tentative fix in place.
Though I have added that 'pelletier' to my neg cases and the test is now failing: and I don't know exactly why (the trace is again overwhelming),
but I guess either I am trading termination for completeness, or this is finally a failure of TNT.
I need a (more) principled approach...
-Julio
Hi,
One of the pelettier test cases was to test
how long it takes to terminate with "false",
the other was to test how long it takes to
terminate with "true". The Prolog time/1
predicate can be used to measure both, a
"false" outcome and a "true" outcome.
Wangs algorithm can be easily extended to
biconditional:
:- op(1100, xfx, <->).
prove(L) :- select((A->B),L,R), !, prove([-A,B|R]).
prove(L) :- select((A<->B),L,R), !, prove([-A,B|R]), prove([-B,A|R]). prove(L) :- select(-(A->B),L,R), !, prove([A|R]), prove([-B|R]).
prove(L) :- select(-(A<->B),L,R), !, prove([-A,-B|R]), prove([B,A|R]). prove(L) :- select(-A,L,R), member(A,R), !.
Usually Theorem Provers choke on these
test cases, unless they work with some
XOR representation inspired by Boolean Rings.
But provers insprired by Boolean Algebra explode:
/* success timing */
?- between(5,10,N), nasty_bicond(N,X),
time(prove([X<->X])), fail; true.
% 211,301 inferences, 0.000 CPU in 0.013 seconds
% 971,051 inferences, 0.047 CPU in 0.060 seconds
% 4,386,029 inferences, 0.266 CPU in 0.270 seconds
% 19,547,363 inferences, 1.219 CPU in 1.209 seconds
% 86,183,093 inferences, 5.141 CPU in 5.355 seconds
% 376,634,555 inferences, 22.969 CPU in 23.355 seconds
true.
/* failure timing */
?- between(5,10,N), nasty_bicond(N,X),
M is N+1, nasty_bicond(M,Y),
time(\+ prove([X<->Y])), fail; true.
% 113,383 inferences, 0.000 CPU in 0.008 seconds
% 514,955 inferences, 0.031 CPU in 0.032 seconds
% 2,308,703 inferences, 0.141 CPU in 0.143 seconds
% 10,233,763 inferences, 0.625 CPU in 0.632 seconds
% 44,928,359 inferences, 2.781 CPU in 2.773 seconds
% 195,659,867 inferences, 12.078 CPU in 12.142 seconds
true.
The pelletier test case generator:
nasty_bicond(0, x0) :- !.
nasty_bicond(N, (X<->Y)) :-
number_codes(N, L),
atom_codes(X, [0'x|L]),
M is N-1,
nasty_bicond(M, Y).
What is a Boolean Ring:
https://en.wikipedia.org/wiki/Boolean_ring
What is a Boolean Algebra: https://en.wikipedia.org/wiki/Boolean_algebra_%28structure%29
Julio Di Egidio schrieb:
On 05/12/2024 22:26, Julio Di Egidio wrote:
On 02/12/2024 12:37, Julio Di Egidio wrote:
On 02/12/2024 09:49, Mild Shock wrote:
Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
The solver *is* very slow at the moment, and you are trying to prove
a too complicated statement:
```
?- unfold(tnt((p<->(q<->r))<->(p<->q)), X).
```
That 'pelletier' is actually false. I guess you have miscopied it,
this one is true (classically):
`((p <-> (q <-> r)) <-> (p <-> q)) <-> r`.
Meanwhile, I have narrowed the problem of non-termination down to the
imp-elim rule, and already have a tentative fix in place.
Though I have added that 'pelletier' to my neg cases and the test is
now failing: and I don't know exactly why (the trace is again
overwhelming), but I guess either I am trading termination for
completeness, or this is finally a failure of TNT.
I need a (more) principled approach...
-Julio
Ok, what helps here is reordering the rules:
prove(L) :- select(-A,L,R), member(A,R), !.
prove(L) :- select((A->B),L,R), !, prove([-A,B|R]).
prove(L) :- select((A<->B),L,R), !, prove([-A,B|R]), prove([-B,A|R]). prove(L) :- select(-(A->B),L,R), !, prove([A|R]), prove([-B|R]).
prove(L) :- select(-(A<->B),L,R), !, prove([-A,-B|R]), prove([B,A|R]).
The above runs fast in the previous test cases, since
Axiom does not need to work with atoms anymore, and
syntactically equivalent formulas are found by Prolog
unification. But we can make the test case more difficult,
by swapping sides:
% nasty1(+Integer, -Expr)
nasty1(0, x0) :- !.
nasty1(N, (X<->Y)) :-
number_codes(N, L),
atom_codes(X, [0'x|L]),
M is N-1,
nasty1(M, Y).
% nasty1(+Integer, -Expr)
nasty1(0, x0) :- !.
nasty1(N, (X<->Y)) :-
number_codes(N, L),
atom_codes(X, [0'x|L]),
M is N-1,
nasty1(M, Y).
Now the picture is again not very favorable, despite
we did an early non atomic Axiom test in prove/1:
/* success timing */
?- between(5,10,N), nasty1(N,X), nasty2(N,Y),
time(prove([X<->Y])), fail; true.
% 38,207 inferences, 0.000 CPU in 0.002 seconds
% 111,919 inferences, 0.000 CPU in 0.006 seconds
% 314,127 inferences, 0.016 CPU in 0.017 seconds
% 852,143 inferences, 0.031 CPU in 0.045 seconds
% 2,248,175 inferences, 0.109 CPU in 0.117 seconds
% 5,795,311 inferences, 0.281 CPU in 0.299 seconds
true.
/* failure timing */
?- between(5,10,N), nasty1(N,X), nasty2(N,Y),
time(\+ prove([(X<->(q<->Y))])), fail; true.
% 23,651 inferences, 0.000 CPU in 0.002 seconds
% 66,537 inferences, 0.000 CPU in 0.004 seconds
% 182,047 inferences, 0.000 CPU in 0.010 seconds
% 485,421 inferences, 0.000 CPU in 0.025 seconds
% 1,264,835 inferences, 0.047 CPU in 0.065 seconds
% 3,229,393 inferences, 0.156 CPU in 0.165 seconds
true.
The input size grows linearly but the execution
time grows exponential.
Mild Shock schrieb:
Hi,
One of the pelettier test cases was to test
how long it takes to terminate with "false",
the other was to test how long it takes to
terminate with "true". The Prolog time/1
predicate can be used to measure both, a
"false" outcome and a "true" outcome.
Wangs algorithm can be easily extended to
biconditional:
:- op(1100, xfx, <->).
prove(L) :- select((A->B),L,R), !, prove([-A,B|R]).
prove(L) :- select((A<->B),L,R), !, prove([-A,B|R]), prove([-B,A|R]).
prove(L) :- select(-(A->B),L,R), !, prove([A|R]), prove([-B|R]).
prove(L) :- select(-(A<->B),L,R), !, prove([-A,-B|R]), prove([B,A|R]).
prove(L) :- select(-A,L,R), member(A,R), !.
Usually Theorem Provers choke on these
test cases, unless they work with some
XOR representation inspired by Boolean Rings.
But provers insprired by Boolean Algebra explode:
/* success timing */
?- between(5,10,N), nasty_bicond(N,X),
time(prove([X<->X])), fail; true.
% 211,301 inferences, 0.000 CPU in 0.013 seconds
% 971,051 inferences, 0.047 CPU in 0.060 seconds
% 4,386,029 inferences, 0.266 CPU in 0.270 seconds
% 19,547,363 inferences, 1.219 CPU in 1.209 seconds
% 86,183,093 inferences, 5.141 CPU in 5.355 seconds
% 376,634,555 inferences, 22.969 CPU in 23.355 seconds
true.
/* failure timing */
?- between(5,10,N), nasty_bicond(N,X),
M is N+1, nasty_bicond(M,Y),
time(\+ prove([X<->Y])), fail; true.
% 113,383 inferences, 0.000 CPU in 0.008 seconds
% 514,955 inferences, 0.031 CPU in 0.032 seconds
% 2,308,703 inferences, 0.141 CPU in 0.143 seconds
% 10,233,763 inferences, 0.625 CPU in 0.632 seconds
% 44,928,359 inferences, 2.781 CPU in 2.773 seconds
% 195,659,867 inferences, 12.078 CPU in 12.142 seconds
true.
The pelletier test case generator:
nasty_bicond(0, x0) :- !.
nasty_bicond(N, (X<->Y)) :-
number_codes(N, L),
atom_codes(X, [0'x|L]),
M is N-1,
nasty_bicond(M, Y).
What is a Boolean Ring:
https://en.wikipedia.org/wiki/Boolean_ring
What is a Boolean Algebra:
https://en.wikipedia.org/wiki/Boolean_algebra_%28structure%29
Julio Di Egidio schrieb:
On 05/12/2024 22:26, Julio Di Egidio wrote:
On 02/12/2024 12:37, Julio Di Egidio wrote:
On 02/12/2024 09:49, Mild Shock wrote:
Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
The solver *is* very slow at the moment, and you are trying to
prove a too complicated statement:
```
?- unfold(tnt((p<->(q<->r))<->(p<->q)), X).
```
That 'pelletier' is actually false. I guess you have miscopied it,
this one is true (classically):
`((p <-> (q <-> r)) <-> (p <-> q)) <-> r`.
Meanwhile, I have narrowed the problem of non-termination down to the
imp-elim rule, and already have a tentative fix in place.
Though I have added that 'pelletier' to my neg cases and the test is
now failing: and I don't know exactly why (the trace is again
overwhelming), but I guess either I am trading termination for
completeness, or this is finally a failure of TNT.
I need a (more) principled approach...
-Julio
One of the pelettier test cases was to test
how long it takes to terminate with "false",
the other was to test how long it takes to
terminate with "true". The Prolog time/1
Wangs algorithm can be easily extended to biconditional:
7,d->8] applied, by this little Declarative (What) code:
Looks like uncontrolled confluence, which usually
happens when you write down rules declaratively.
There are some nice pictures:
Wolfram, S. A New Kind of Science. Champaign, IL:
Wolfram Media, pp. 507 and 1036-1037, 2002. https://mathworld.wolfram.com/Confluent.html
Showing how search explodes, by doing redundant work.
Mild Shock schrieb:
Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
?- solve_case(TT, pelletier, G), time(solve_t__sel(TT, G)).
Action (h for help) ? abort
% 844,501,974 inferences, 63.891 CPU in 68.236 seconds (94% CPU,
13217933 Lips)
% Execution Aborted
The test case was:
solve_case(neg, pelletier, []=>((p<->(q<->r))<->(p<->q))).
Or just a problem of explosion?
Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
?- solve_case(TT, pelletier, G), time(solve_t__sel(TT, G)).
Action (h for help) ? abort
% 844,501,974 inferences, 63.891 CPU in 68.236 seconds (94% CPU,
13217933 Lips)
% Execution Aborted
The test case was:
solve_case(neg, pelletier, []=>((p<->(q<->r))<->(p<->q))).
Or just a problem of explosion?
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 715 |
| Nodes: | 16 (2 / 14) |
| Uptime: | 22:15:40 |
| Calls: | 12,105 |
| Calls today: | 5 |
| Files: | 15,006 |
| Messages: | 6,518,126 |
