Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]


Groups > comp.lang.prolog > #12550

Re: France is the Fire Nation of Prolog

From Mostowski Collapse <janburse@fastmail.fm>
Newsgroups comp.lang.prolog
Subject Re: France is the Fire Nation of Prolog
Date 2022-01-23 01:32 +0100
Message-ID <ssi7mg$1c1s$3@solani.org> (permalink)
References <d1ab4350-9a9d-49bc-845b-f10eeb1ec763n@googlegroups.com> <sshgke$v0t$1@solani.org>

Show all headers | View raw


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

Back to comp.lang.prolog | Previous | NextPrevious in thread | Next in thread | Find similar | Unroll thread


Thread

France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-07-21 06:41 -0700
  Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-07-21 06:48 -0700
    Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-07-22 03:51 -0700
      Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-07-22 03:53 -0700
        Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-07-23 03:32 -0700
          Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-07-23 03:46 -0700
            Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-07-28 02:19 -0700
              Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-07-28 02:29 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-07-28 02:42 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-10-26 00:57 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-10-26 00:58 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-10-26 00:59 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-03 07:47 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-03 07:48 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-04 00:49 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-04 00:50 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-06 12:07 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-06 12:08 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-06 12:09 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-10 03:56 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-10 03:58 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-15 18:46 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-15 18:54 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-25 04:25 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-28 07:22 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-28 07:29 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-28 11:31 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-28 15:20 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-28 15:24 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-11-30 06:07 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-12-15 04:42 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-12-17 08:59 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-12-28 10:26 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-12-29 14:46 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <janburse@fastmail.fm> - 2021-12-30 09:56 +0100
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-12-30 01:06 -0800
                Re: France is the Fire Nation of Prolog Julio Di Egidio <julio@diegidio.name> - 2021-12-30 02:48 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2021-12-30 04:38 -0800
  Re: France is the Fire Nation of Prolog Mostowski Collapse <janburse@fastmail.fm> - 2021-12-31 01:11 +0100
    Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-01 03:30 -0800
      Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-02 15:28 -0800
        Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-04 02:49 -0800
          Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-04 03:28 -0800
            Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-04 03:46 -0800
              Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-08 05:06 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-08 07:57 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-09 00:30 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-09 00:58 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-16 17:58 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-18 07:57 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-20 06:03 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-20 06:06 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-22 09:52 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-23 13:02 -0800
  Re: France is the Fire Nation of Prolog Mostowski Collapse <janburse@fastmail.fm> - 2022-01-22 18:58 +0100
    Re: France is the Fire Nation of Prolog Mostowski Collapse <janburse@fastmail.fm> - 2022-01-23 01:32 +0100
      Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-23 07:54 -0800
        Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-24 02:38 -0800
          Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-30 12:10 -0800
            Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-30 12:15 -0800
              Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-01-30 12:21 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-02-08 03:28 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-02-10 08:27 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-02-10 08:29 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-02-12 05:02 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-02-14 03:59 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-02-14 09:35 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-02-14 10:42 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-07-09 01:12 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-07-09 01:36 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-07-09 01:49 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-09-14 09:21 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-09-14 09:25 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2022-09-14 09:38 -0700
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2023-01-12 05:16 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2023-01-12 05:17 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2023-02-08 11:25 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2023-02-14 01:46 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2023-02-14 01:49 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2023-02-14 02:27 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2023-02-14 05:55 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2023-02-16 13:30 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2023-02-16 15:39 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2023-02-20 01:28 -0800
                Re: France is the Fire Nation of Prolog Mostowski Collapse <bursejan@gmail.com> - 2023-02-20 01:30 -0800
                Re: France is the Fire Nation of Prolog Mild Shock <bursejan@gmail.com> - 2023-10-10 15:54 -0700
                Re: France is the Fire Nation of Prolog Mild Shock <bursejan@gmail.com> - 2023-10-10 16:08 -0700
                Why cant Scryer Prolog parse this? (Was: France is the Fire Nation of Prolog) Mild Shock <janburse@fastmail.fm> - 2024-09-01 15:22 +0200
                Re: Why cant Scryer Prolog parse this? (Was: France is the Fire Nation of Prolog) Mild Shock <janburse@fastmail.fm> - 2024-09-01 16:03 +0200
                Re: Why cant Scryer Prolog parse this? (Was: France is the Fire Nation of Prolog) Mild Shock <janburse@fastmail.fm> - 2024-09-01 16:29 +0200
                Re: Why cant Scryer Prolog parse this? (Was: France is the Fire Nation of Prolog) Mild Shock <janburse@fastmail.fm> - 2024-09-01 19:05 +0200

csiph-web