Hi,
Refering to this idea:
leanTAP revisited - Melvin Fitting
https://www.researchgate.net/publication/2240690
Some benchmark results:
/* non-leanTap, prefers A->B over other forms */
?- urquhart(12,X), time(prove([X])).
% Zeit 2104 ms, GC 16 ms, Lips 6894483, Uhr 09.12.2024 15:15
/* leanTap, works strictly left to right */
?- urquhart(12,X), time(prove2([X],[])).
% Zeit 81174 ms, GC 0 ms, Lips 6679748, Uhr 09.12.2024 15:12
The source code:
/* non-leanTap, prefers A->B over other forms */
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]).
/* leanTap, works strictly left to right */
prove2([(A->B)|L],R) :- !, prove2([-A,B|L],R).
prove2([(A<->B)|L],R) :- !, prove2([-A,B|L],R), prove2([-B,A|L],R).
prove2([- (A->B)|L],R) :- !, prove2([A|L],R), prove2([-B|L],R).
prove2([- (A<->B)|L],R) :- !, prove2([-A,-B|L],R), prove2([B,A|L],R). prove2([A|_],R) :- member(-A,R), !.
prove2([-A|_],R) :- member(A,R), !.
prove2([A|L],R) :- prove2(L,[A|R]).
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
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)