How to use of upcase_atom/2 to get uppercase letters in an output

Help! Data Structure
43

Thanks, I am learning. It will be the occasion of seeing how implementing iterative deepening. If I am not mistaken, Otten uses it for his leanseq_v5.pl, that is his prover for 1st order logic.

I add that I just tested your Prolog rule for => elimination in the following format in interative deepening, if I am not mistaken, this code is leanseq_v5.pl from Otten’s work:

prove(G>D,FV,I,J,K,eimpl(G > D, P1, P2)) :-
     select(B,D,D1),
     prove(G>[A|D1],FV,I,J,J1,P1),
     prove(G> [(A=>B)|D1],FV,I,J1,K,P2).

But it loops:

?- provable((((a=>b)&a)=>b),Proof).
iteration:1

:frowning:

45

No difficulty with this. The difficulty is for me always the Prolog implementation.

52

Prolog purism. Congratulations ! :grinning:

55

The fact that a propositional prover is incomplete vis-à-vis FOL matrices is not vey worrying, in my opinion, because syntactically, FOL matrices belong to the first order predicate calculus, not to propositional calculus. The examples you gave are correctly treated by Jens Otten’s leanseq_v5.pl :

?- prove((p(X) => p(t) | p(s)) & (p(X) => p(s))).
iteration:1
% 26,419 inferences, 0.014 CPU in 0.014 seconds (100% CPU, 1876009 Lips)
X = s.

?- prove((p(Y,Y)=>p(X,f(X)))).
iteration:1
iteration:2
iteration:3
iteration:4
iteration:5
iteration:6
iteration:7
iteration:8
iteration:9
iteration:10
iteration:11
iteration:12
iteration:13
iteration:14
iteration:15
iteration:16
iteration:17
iteration:18
iteration:19
iteration:20
iteration:21
iteration:22
iteration:23
iteration:24
iteration:25
iteration:26
iteration:27
iteration:28
iteration:29
iteration:30
iteration:31
iteration:32
iteration:33
iteration:34
iteration:35
iteration:36
iteration:37
iteration:38
iteration:39
iteration:40
iteration:41
iteration:42
iteration:43
iteration:44
iteration:45
iteration:46
iteration:47
iteration:48
iteration:49
iteration:50
.
.
.

the iteration does not stop, showing that the formula is invalid (this program does not give countermodel, but it is nevertheless correct).

58

The order of rules in Zucker-Otten’s leanseq_v2.pl is not efficient. Non-branching rules must be before the branching ones. If you compare this result with the result obtained by a fork of this prover, you get a better sequent proof.
Best wishes, an happy new year

60

That’s interesting, thanks.
From a logical point of view, if I understand correctly, the difference is that the Weakening rules are built in rules L& and Rv (in your LK), and there are built-in in the Axiom or Init rule in Otten’s program.

62

Thanks, again, it is very interesting and I will try to follow your code to get a genuine LK prover.
Did you test the efficiency of your prover?
My fork succeds in proving Pelletier problem 17 i.e. the following classical theorem :

( p_1
  <=> ( p_2
    <=> ( p_3
      <=> ( p_4
        <=> ( p_5
          <=> ( p_6
            <=> ( p_7
              <=> ( p_8
                <=> ( p_9
                  <=> ( p_10
                    <=> ( p_11
                      <=> ( p_12
                        <=> ( p_13
                          <=> ( p_14
                            <=> ( p_1
                              <=> ( p_2
                                <=> ( p_3
                                  <=> ( p_4
                                    <=> ( p_5
                                      <=> ( p_6
                                        <=> ( p_7
                                          <=> ( p_8
                                            <=> ( p_9
                                              <=> ( p_10
                                                <=> ( p_11
                                                  <=> ( p_12
                                                    <=> ( p_13
                                                      <=> p_14 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )

On your website, I get :

error(syntax_error(parenthesis_balance), _0)

but I checked the parenthesis balance with emacs and it is correct. On my website, the same formula is unprovable probably because of time limitations. But it is provable locally with my fork via emacs:

% 54,890,488 inferences, 4.483 CPU in 4.487 seconds (100% CPU, 12244554 Lips)

I do not paste here the output Prolog proof, it is too big.

63

I just tested the proof of Pelletier problem 17 with swipl simple_server.pl and it works, Firefox provides the proof and one can read on the terminal:

% 54,890,488 inferences, 4.423 CPU in 4.424 seconds (100% CPU, 12409457 Lips)

Security worries apart, that would be a good solution for Prolog provers online.

66

Your LK prover is very fast. Great !

EDIT:
I have tested my zdd based refutation prover for the Pelletier problem 17 with N = 15, which took time about one hour. I have little knowledge to say about LK, and perhaps have no time to learn it. Anyway thank you for showing power of LK prover.

% ?- time((N=15, numlist(1, N, Ns), maplist(pred([X, p(X)]), Ns, Ps),
%	append(Qs, [Last], Ps),  append(Ps, Qs, Rs),
%	foldl(pred([X, Y, <->(X, Y)]), Rs, Last, Z),
%	open_state(S), prop_neg_refute(Z, S))).
%@ VALID
%@ % 66,842,271,417 inferences, 3656.633 CPU in 29010.983 seconds (13% CPU, 18279732 Lips)
%@ N = 15,
%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
%@ Ps = [p(1), p(2), p(3), p(4), p(5), p(6), p(7), p(8), p(...)|...],
%@ Qs = [p(1), p(2), p(3), p(4), p(5), p(6), p(7), p(8), p(...)|...],
%@ Last = p(15),
%@ Rs = [p(1), p(2), p(3), p(4), p(5), p(6), p(7), p(8), p(...)|...],
%@ Z = <->(p(14), <->(p(13), <->(p(12), <->(p(11), <->(p(10), <->(p(9), <->(p(8), <->(p(7), <->(p(...), <->(..., ...)))))))))),
%@ S = .. .

EDIT: I have noticed that reverse must be inserted as follows. I hope
this keeps validity of the formula, where = is for logical equivalence.

% ?- time((N=5, numlist(1, N, Ns), maplist(pred([X, p(X)]), Ns, Ps),
%	append(Qs, [Last], Ps),  append(Ps, Qs, Rs), reverse(Rs, Us),
%	foldl(pred([X, Y, =(X, Y)]), Us, Last, Z),
%	writeln(Z),
%	open_state(S), prop_neg_refute(Z, S))).
%@ p(1)=(p(2)=(p(3)=(p(4)=(p(5)=(p(1)=(p(2)=(p(3)=(p(4)=p(5)))))))))
%@ VALID
%@ % 119,292 inferences, 0.009 CPU in 0.009 seconds (97% CPU, 13802152 Lips)
%@ N = 5,
<snip>
67

Thanks for your note.
First, the rules for the connectives are LK’s, but it is not a genuine LK prover, because of the lack of structural rules: Weakening for example is built-in the Axiom. More, there is no refutation rule in LK, of course.
Second, the efficiency of this Prolog classical prover is based on two changes I made starting from the fork of Jens Otten’s leanseq_v2.pl made by Philip Zucker on his personal blog (see the link above in this discussion):

  1. Thanks to a suggestion made by TA_intern on this forum, I replaced select1 by the deterministic SWI-Prolog predicate select/3. (See also this discussion.)
  2. Then, the definition of select1 via append was useless, and therefore I removed the following lines of code
% -----------------------------------------------------------------
select1(X,L,L1) :- append(L2,[X|L3],L), append(L2,L3,L1).
% -----------------------------------------------------------------

from Zucker’s fork. It is well known that append is a cause of inefficiency .

That’s it.

Now, it is maybe possible both to preserve the efficiency of this prover and to transform it into a genuine LK prover thank to @j4n_bur53’s fork. . But I haven’t taken the time to try it yet.

69

Thanks for this suggestion. I began to try to adapt leanseq_v5.pl, but I met an error with Tau Prolog, while all was correct with SWI. I am always impressed by your quickness. Unfortunately, I have to grade students now, and I am not available during next days.
Thanks again !

71

Suspecting that my refutation prover for the Pelletier problem takes time for converting given formula into a set of clauses for refutation method, I added four lines to the prover for use of hash table memo from curiosity. The effect is dramatic ! Now it takes only less than a minuet even for N =100.
EDIT:
I do not intend to make noise for your current work, but rather have strong interest in LK/LJ/NK/NJ. Once I was a little bit close to logic community in Japan, and had opportunities to listen to their lectures on cut elimination and proof normalization etc, though almost nothing remains in my active memory but respect to such logic people.

EDIT
“.” and “+” signs below in the log are printed each time of maching hashed keys, which supports my suspicion above.

.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+.+
73

Thank you for references. “Less than 1 mili seconds” is amazing.

However it sounds reasonable for me, because
I checked that almost 100% of the total time for my case is spent for preprocessing, and the time for general refutation procedure proper is less than about 0.2 seconds, i.e. negligible compared with the preprocessing.

%@ % 1,694,993 inferences, 0.173 CPU in 0.173 seconds (100% CPU, 9792496 Lips)

%@ VALID
%@ % 491,556,942 inferences, 44.378 CPU in 46.291 seconds (96% CPU, 11076523 Lips)
76

Thanks for the codes. It would be useful when zdd over the boolean ring is considered. So far my zdd works only over the totally ordered atoms or the boolean algebra. Fortunately behavior of the latter is close to the other as you would see the codes (library(pac/zdd.pl)) by way of selecting a natural ordering of the literals. I am not far from sure that such extended zdd would be useful for SAT problem. I am pessimistic for such extensions without confidence, but added it in my future plan.

79

Thanks, but linear logic is too much complicated for me. I dislike this logic, even if it was invented by a French logician…

81

About the
dislike and likes of Russian logicians by @joseph-vidal-rosset I don’t know.

:slight_smile: I esteem them.

84

Hello. Again the order of rules in Zucker-Otten’s prolog prover explains this result. My fork provides a non-branching proof, while yours adds interestingly what is “vacuous discharge” in Natural Deduction (ND). I never saw “vacuous discharge” in Sequent Calculus (SC), because its corresponds to useless Weakening on the left. Jan von Plato and Sara Negri explained translations between ND and SC in their excellent book. Last point, your axiom in your new fork is clearly non standard. Have a nice Sunday .

87

Thanks for these explanations !

90

I never said that any Weakening is useless, but in the example you gave, it is a useless Weakening: if there is a theorem on the right of the turnstile of a sequent, any formula on the left is useless to prove such a sequent.

93

I looked at your code and I am unable to imitate it to close this gap. There is no Prolog output in your fork and I do not get neither latex(P,V) nor [] instead of Proof in the query. Your explanations are not enough developped for me, maybe for others, but not for me.