Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.prolog > #12549
| From | Mostowski Collapse <janburse@fastmail.fm> |
|---|---|
| Newsgroups | comp.lang.prolog |
| Subject | Re: France is the Fire Nation of Prolog |
| Date | 2022-01-22 18:58 +0100 |
| Message-ID | <sshgke$v0t$1@solani.org> (permalink) |
| References | <d1ab4350-9a9d-49bc-845b-f10eeb1ec763n@googlegroups.com> |
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 | Next — Previous in thread | Next in thread | Find similar | Unroll 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