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

Groups > comp.lang.prolog > #12143 > unrolled thread

France is the Fire Nation of Prolog

Back to article view | Back to comp.lang.prolog

Contents

  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

Page 3 of 5 — ← Prev page 1 2 [3] 4 5  Next page →

#12518

Oki Doki, full first order logic can be also rendered now:

Leibniz’s Dream in Dogelog Player
https://twitter.com/dogelogch/status/1477779371628933121

Leibniz’s Dream in Dogelog Player
https://www.facebook.com/groups/dogelog

Mostowski Collapse schrieb am Samstag, 1. Januar 2022 um 12:30:25 UTC+1:
> So how was it done? First one needs to reduce proof noise: 
> 
> Dogelog Player removes proof noise 
> https://twitter.com/dogelogch/status/1477236879795830785 
> 
> Dogelog Player removes proof noise 
> https://www.facebook.com/groups/dogelog
> Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1: 
> > Lean TAP can be fun. Spent the whole day to 
> > render MathJax. Then was annoyed by MathJax, 
> > how do you put this thingy into an email? 
> > 
> > So here is barber paradox in list form with Unicode: 
> > 
> > 1. s(a,a) ⊢ s(a,a) (ax) 
> > 2. s(a,a) ⊢ ∃zs(z,z) (R∃) 
> > 3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬) 
> > 4. s(a,a) ⊢ s(a,a) (ax) 
> > 5. s(a,a) ⊢ ∃zs(z,z) (R∃) 
> > 6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3) 
> > 7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀) 
> > 8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃) 
> > 9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒) 
> > 
> > http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

[toc] | [prev] | [next] | [standalone]

#12519

I am afraid, I didn't post the full Barber Paradox. I only posted 
what was found in Jens Ottens ex_barber.pl. Now a regret not 
providing (<=>)/2 in my leanseq_v5.pl fork. The two sided barber 
paradox cannot so concisely be formulate without (<=>)/2.

What would be fun is not only XOR-SAT but also XOR-FOL.
The Jens Otten provers can solve FOL problems among which 
we also find FOL problems in prenex normal form Q1x1…QnxnM 

where Q1,…,Qn are the alternating quantifier blocks and M is
 the FOL matrix. Quantifiers are handled in Jens Otten provers:

    Qj=∀: is handled by a Skolem function.
    Qj=∃: is handled by fresh variable and contraction.

Besides that all the 3 provers he presents, leanseq_v5.pl, 
leantap_pure.pl and leancop_pure.pl do the same with the 
FOL matrix M, they put it into conjunctive normal form (CNF), 
and try to solve it via unification. Lets take the Barber Paradox 

and see how the CNF looks like. The Barber Paradox with (<=>)/2:

¬∃x∀y(¬s(y,y) <=> s(x,y))

The Barber Paradox in prenex with CNF:

∀x∃y((¬s(y,y) | s(x,y)) & (s(y,y) | ¬s(x,y))

When the above is solved unification wise the same thing 
happens twice for both conjuncts. But since the XOR-SAT 
rewriting prototype has simp(A=A, 1) does this mean we could 
solve XOR-FOL differently and for example have a FOL matrix 

format where we solve P<=>Q by directly trying to unify P and Q?

Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 00:29:00 UTC+1:
> Oki Doki, full first order logic can be also rendered now: 
> 
> Leibniz’s Dream in Dogelog Player 
> https://twitter.com/dogelogch/status/1477779371628933121 
> 
> Leibniz’s Dream in Dogelog Player 
> https://www.facebook.com/groups/dogelog
> Mostowski Collapse schrieb am Samstag, 1. Januar 2022 um 12:30:25 UTC+1: 
> > So how was it done? First one needs to reduce proof noise: 
> > 
> > Dogelog Player removes proof noise 
> > https://twitter.com/dogelogch/status/1477236879795830785 
> > 
> > Dogelog Player removes proof noise 
> > https://www.facebook.com/groups/dogelog 
> > Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1: 
> > > Lean TAP can be fun. Spent the whole day to 
> > > render MathJax. Then was annoyed by MathJax, 
> > > how do you put this thingy into an email? 
> > > 
> > > So here is barber paradox in list form with Unicode: 
> > > 
> > > 1. s(a,a) ⊢ s(a,a) (ax) 
> > > 2. s(a,a) ⊢ ∃zs(z,z) (R∃) 
> > > 3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬) 
> > > 4. s(a,a) ⊢ s(a,a) (ax) 
> > > 5. s(a,a) ⊢ ∃zs(z,z) (R∃) 
> > > 6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3) 
> > > 7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀) 
> > > 8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃) 
> > > 9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒) 
> > > 
> > > http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

[toc] | [prev] | [next] | [standalone]

#12520

Nice! Now the example runs also from within Python. Even 
on ordinary CMD on Windows 10. Just use for example this 
font *NSimSum*, select it in the console properties.

See also:

Unicode Proof Listing in Dogelog Player
https://twitter.com/dogelogch/status/1478315286491287553

Unicode Proof Listing in Dogelog Player
https://www.facebook.com/groups/dogelog

But I have to simplify the Python Dogelog Player console.
Now the Python Dogelog Player console is a tutorial example,
but dogelog.py should do it by default.

Please be patient.

Mostowski Collapse schrieb am Dienstag, 4. Januar 2022 um 11:49:53 UTC+1:
> I am afraid, I didn't post the full Barber Paradox. I only posted 
> what was found in Jens Ottens ex_barber.pl. Now a regret not 
> providing (<=>)/2 in my leanseq_v5.pl fork. The two sided barber 
> paradox cannot so concisely be formulate without (<=>)/2. 
> 
> What would be fun is not only XOR-SAT but also XOR-FOL. 
> The Jens Otten provers can solve FOL problems among which 
> we also find FOL problems in prenex normal form Q1x1…QnxnM 
> 
> where Q1,…,Qn are the alternating quantifier blocks and M is 
> the FOL matrix. Quantifiers are handled in Jens Otten provers: 
> 
> Qj=∀: is handled by a Skolem function. 
> Qj=∃: is handled by fresh variable and contraction. 
> 
> Besides that all the 3 provers he presents, leanseq_v5.pl, 
> leantap_pure.pl and leancop_pure.pl do the same with the 
> FOL matrix M, they put it into conjunctive normal form (CNF), 
> and try to solve it via unification. Lets take the Barber Paradox 
> 
> and see how the CNF looks like. The Barber Paradox with (<=>)/2: 
> 
> ¬∃x∀y(¬s(y,y) <=> s(x,y)) 
> 
> The Barber Paradox in prenex with CNF: 
> 
> ∀x∃y((¬s(y,y) | s(x,y)) & (s(y,y) | ¬s(x,y)) 
> 
> When the above is solved unification wise the same thing 
> happens twice for both conjuncts. But since the XOR-SAT 
> rewriting prototype has simp(A=A, 1) does this mean we could 
> solve XOR-FOL differently and for example have a FOL matrix 
> 
> format where we solve P<=>Q by directly trying to unify P and Q?
> Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 00:29:00 UTC+1: 
> > Oki Doki, full first order logic can be also rendered now: 
> > 
> > Leibniz’s Dream in Dogelog Player 
> > https://twitter.com/dogelogch/status/1477779371628933121 
> > 
> > Leibniz’s Dream in Dogelog Player 
> > https://www.facebook.com/groups/dogelog 
> > Mostowski Collapse schrieb am Samstag, 1. Januar 2022 um 12:30:25 UTC+1: 
> > > So how was it done? First one needs to reduce proof noise: 
> > > 
> > > Dogelog Player removes proof noise 
> > > https://twitter.com/dogelogch/status/1477236879795830785 
> > > 
> > > Dogelog Player removes proof noise 
> > > https://www.facebook.com/groups/dogelog 
> > > Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1: 
> > > > Lean TAP can be fun. Spent the whole day to 
> > > > render MathJax. Then was annoyed by MathJax, 
> > > > how do you put this thingy into an email? 
> > > > 
> > > > So here is barber paradox in list form with Unicode: 
> > > > 
> > > > 1. s(a,a) ⊢ s(a,a) (ax) 
> > > > 2. s(a,a) ⊢ ∃zs(z,z) (R∃) 
> > > > 3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬) 
> > > > 4. s(a,a) ⊢ s(a,a) (ax) 
> > > > 5. s(a,a) ⊢ ∃zs(z,z) (R∃) 
> > > > 6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3) 
> > > > 7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀) 
> > > > 8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃) 
> > > > 9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒) 
> > > > 
> > > > http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

[toc] | [prev] | [next] | [standalone]

#12521

Holy cow, the monke army is in full bloom, now
#Python trending on Twitter!!! So “Digital Twin” 
is the new name for software agent?

https://towardsdatascience.com/digital-twin-with-python-a-hands-on-example-2a3036124b61

Mostowski Collapse schrieb am Dienstag, 4. Januar 2022 um 12:28:22 UTC+1:
> Nice! Now the example runs also from within Python. Even 
> on ordinary CMD on Windows 10. Just use for example this 
> font *NSimSum*, select it in the console properties. 
> 
> See also: 
> 
> Unicode Proof Listing in Dogelog Player 
> https://twitter.com/dogelogch/status/1478315286491287553 
> 
> Unicode Proof Listing in Dogelog Player 
> https://www.facebook.com/groups/dogelog 
> 
> But I have to simplify the Python Dogelog Player console. 
> Now the Python Dogelog Player console is a tutorial example, 
> but dogelog.py should do it by default. 
> 
> Please be patient.
> Mostowski Collapse schrieb am Dienstag, 4. Januar 2022 um 11:49:53 UTC+1: 
> > I am afraid, I didn't post the full Barber Paradox. I only posted 
> > what was found in Jens Ottens ex_barber.pl. Now a regret not 
> > providing (<=>)/2 in my leanseq_v5.pl fork. The two sided barber 
> > paradox cannot so concisely be formulate without (<=>)/2. 
> > 
> > What would be fun is not only XOR-SAT but also XOR-FOL. 
> > The Jens Otten provers can solve FOL problems among which 
> > we also find FOL problems in prenex normal form Q1x1…QnxnM 
> > 
> > where Q1,…,Qn are the alternating quantifier blocks and M is 
> > the FOL matrix. Quantifiers are handled in Jens Otten provers: 
> > 
> > Qj=∀: is handled by a Skolem function. 
> > Qj=∃: is handled by fresh variable and contraction. 
> > 
> > Besides that all the 3 provers he presents, leanseq_v5.pl, 
> > leantap_pure.pl and leancop_pure.pl do the same with the 
> > FOL matrix M, they put it into conjunctive normal form (CNF), 
> > and try to solve it via unification. Lets take the Barber Paradox 
> > 
> > and see how the CNF looks like. The Barber Paradox with (<=>)/2: 
> > 
> > ¬∃x∀y(¬s(y,y) <=> s(x,y)) 
> > 
> > The Barber Paradox in prenex with CNF: 
> > 
> > ∀x∃y((¬s(y,y) | s(x,y)) & (s(y,y) | ¬s(x,y)) 
> > 
> > When the above is solved unification wise the same thing 
> > happens twice for both conjuncts. But since the XOR-SAT 
> > rewriting prototype has simp(A=A, 1) does this mean we could 
> > solve XOR-FOL differently and for example have a FOL matrix 
> > 
> > format where we solve P<=>Q by directly trying to unify P and Q? 
> > Mostowski Collapse schrieb am Montag, 3. Januar 2022 um 00:29:00 UTC+1: 
> > > Oki Doki, full first order logic can be also rendered now: 
> > > 
> > > Leibniz’s Dream in Dogelog Player 
> > > https://twitter.com/dogelogch/status/1477779371628933121 
> > > 
> > > Leibniz’s Dream in Dogelog Player 
> > > https://www.facebook.com/groups/dogelog 
> > > Mostowski Collapse schrieb am Samstag, 1. Januar 2022 um 12:30:25 UTC+1: 
> > > > So how was it done? First one needs to reduce proof noise: 
> > > > 
> > > > Dogelog Player removes proof noise 
> > > > https://twitter.com/dogelogch/status/1477236879795830785 
> > > > 
> > > > Dogelog Player removes proof noise 
> > > > https://www.facebook.com/groups/dogelog 
> > > > Mostowski Collapse schrieb am Freitag, 31. Dezember 2021 um 01:11:37 UTC+1: 
> > > > > Lean TAP can be fun. Spent the whole day to 
> > > > > render MathJax. Then was annoyed by MathJax, 
> > > > > how do you put this thingy into an email? 
> > > > > 
> > > > > So here is barber paradox in list form with Unicode: 
> > > > > 
> > > > > 1. s(a,a) ⊢ s(a,a) (ax) 
> > > > > 2. s(a,a) ⊢ ∃zs(z,z) (R∃) 
> > > > > 3. ⊢ ¬s(a,a), ∃zs(z,z) (R¬) 
> > > > > 4. s(a,a) ⊢ s(a,a) (ax) 
> > > > > 5. s(a,a) ⊢ ∃zs(z,z) (R∃) 
> > > > > 6. ¬s(a,a) ⇒ s(a,a) ⊢ ∃zs(z,z) (L⇒, 3) 
> > > > > 7. ∀y(¬s(y,y) ⇒ s(a,y)) ⊢ ∃zs(z,z) (L∀) 
> > > > > 8. ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⊢ ∃zs(z,z) (L∃) 
> > > > > 9. ⊢ ∃x∀y(¬s(y,y) ⇒ s(x,y)) ⇒ ∃zs(z,z) (R⇒) 
> > > > > 
> > > > > http://www.xlog.ch/izytab/doclet/en/docs/18_live/40_bin2021/paste07/package.html

[toc] | [prev] | [next] | [standalone]

#12523

Now having more fun with Jens Ottens Lean Prover. This
is a nice little example, where 1 contraction doesn’t work,
but 2 contractions work:

?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 1), !.
fail.
?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 2), !.
true.

See also:

Maslovs Method in Dogelog Player
https://twitter.com/dogelogch/status/1479792480908414979

Maslovs Method in Dogelog Player
https://www.facebook.com/groups/dogelog

[toc] | [prev] | [next] | [standalone]

#12524

The problem with the French logician is, that he does not 
get through the thicket of classical logic into the Maslovs method. 
He only shows a translation for intuitionstic logic in the following form:

(∃xA)* := ∃x !A
https://girard.perso.math.cnrs.fr/Synsem.pdf

Given his other definitions for other connectives and quantifiers 
it might work. In his “Table 2: Classical connectives : definition in 
terms of linear logic” he then repeats this translation.

I think his translation works since he has exponentation 
elsewhere outside of the quantifier. But the Maslov method shows 
that the outside exponentation in classical connectives is 

superflous, and that we can put the exponentiation in front 
of a certain quantifier.

Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 14:06:42 UTC+1:
> Now having more fun with Jens Ottens Lean Prover. This 
> is a nice little example, where 1 contraction doesn’t work, 
> but 2 contractions work: 
> 
> ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 1), !. 
> fail. 
> ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 2), !. 
> true. 
> 
> See also: 
> 
> Maslovs Method in Dogelog Player 
> https://twitter.com/dogelogch/status/1479792480908414979 
> 
> Maslovs Method in Dogelog Player 
> https://www.facebook.com/groups/dogelog

[toc] | [prev] | [next] | [standalone]

#12525

One more iteration of our prover:

Proof systems that are based on the Howard-Curry isomorphism 
and that extract proof terms in the lambda calculus are familiar 
to node dropping. Lambda calculus expressions have a notion 
of variable occurence.

/* Eta Reduction */
λx(Mx) ~~> M for x ∉ M

Variable occurence can then be used similarly to has_usage/2 
to shorten proof terms in the form of lambda expressions. A 
prominent reduction rule is seen in the above that goes by 
the name eta reduction.

Our provers do extract terms where we store integer sequent 
indexes of used formulas. For the newest variant we generalized 
the terms to alfa, beta, gamma and delta, but we currently do 
not use a generic binder format.

See also:

Node Dropping for Maslovs Method
https://twitter.com/dogelogch/status/1480091985222451201

Node Dropping for Maslovs Method
https://www.facebook.com/groups/dogelog

Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 16:57:45 UTC+1:
> The problem with the French logician is, that he does not 
> get through the thicket of classical logic into the Maslovs method. 
> He only shows a translation for intuitionstic logic in the following form: 
> 
> (∃xA)* := ∃x !A 
> https://girard.perso.math.cnrs.fr/Synsem.pdf 
> 
> Given his other definitions for other connectives and quantifiers 
> it might work. In his “Table 2: Classical connectives : definition in 
> terms of linear logic” he then repeats this translation. 
> 
> I think his translation works since he has exponentation 
> elsewhere outside of the quantifier. But the Maslov method shows 
> that the outside exponentation in classical connectives is 
> 
> superflous, and that we can put the exponentiation in front 
> of a certain quantifier.
> Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 14:06:42 UTC+1: 
> > Now having more fun with Jens Ottens Lean Prover. This 
> > is a nice little example, where 1 contraction doesn’t work, 
> > but 2 contractions work: 
> > 
> > ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 1), !. 
> > fail. 
> > ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 2), !. 
> > true. 
> > 
> > See also: 
> > 
> > Maslovs Method in Dogelog Player 
> > https://twitter.com/dogelogch/status/1479792480908414979 
> > 
> > Maslovs Method in Dogelog Player 
> > https://www.facebook.com/groups/dogelog

[toc] | [prev] | [next] | [standalone]

#12526

Somehow being less obsessed with Curry-Howard isomorphism
pays off. Everything is Prolog terms, and maybe some of its
arguments are integers. So what? Proofs are anyway finitistic.

I wonder what happens if I would do some meta logic and
strip myself from lambda calculus translations, going without
logical frameworks or higher-order abstract syntax.

Making also ideas of λ-Prolog obsolete. Hm.. 

Mostowski Collapse schrieb am Sonntag, 9. Januar 2022 um 09:30:13 UTC+1:
> One more iteration of our prover: 
> 
> Proof systems that are based on the Howard-Curry isomorphism 
> and that extract proof terms in the lambda calculus are familiar 
> to node dropping. Lambda calculus expressions have a notion 
> of variable occurence. 
> 
> /* Eta Reduction */ 
> λx(Mx) ~~> M for x ∉ M 
> 
> Variable occurence can then be used similarly to has_usage/2 
> to shorten proof terms in the form of lambda expressions. A 
> prominent reduction rule is seen in the above that goes by 
> the name eta reduction. 
> 
> Our provers do extract terms where we store integer sequent 
> indexes of used formulas. For the newest variant we generalized 
> the terms to alfa, beta, gamma and delta, but we currently do 
> not use a generic binder format. 
> 
> See also: 
> 
> Node Dropping for Maslovs Method 
> https://twitter.com/dogelogch/status/1480091985222451201 
> 
> Node Dropping for Maslovs Method 
> https://www.facebook.com/groups/dogelog
> Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 16:57:45 UTC+1: 
> > The problem with the French logician is, that he does not 
> > get through the thicket of classical logic into the Maslovs method. 
> > He only shows a translation for intuitionstic logic in the following form: 
> > 
> > (∃xA)* := ∃x !A 
> > https://girard.perso.math.cnrs.fr/Synsem.pdf 
> > 
> > Given his other definitions for other connectives and quantifiers 
> > it might work. In his “Table 2: Classical connectives : definition in 
> > terms of linear logic” he then repeats this translation. 
> > 
> > I think his translation works since he has exponentation 
> > elsewhere outside of the quantifier. But the Maslov method shows 
> > that the outside exponentation in classical connectives is 
> > 
> > superflous, and that we can put the exponentiation in front 
> > of a certain quantifier. 
> > Mostowski Collapse schrieb am Samstag, 8. Januar 2022 um 14:06:42 UTC+1: 
> > > Now having more fun with Jens Ottens Lean Prover. This 
> > > is a nice little example, where 1 contraction doesn’t work, 
> > > but 2 contractions work: 
> > > 
> > > ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 1), !. 
> > > fail. 
> > > ?- prove0(?[X='x']:![Y='y']:(p(X) | ~p(Y)), 2), !. 
> > > true. 
> > > 
> > > See also: 
> > > 
> > > Maslovs Method in Dogelog Player 
> > > https://twitter.com/dogelogch/status/1479792480908414979 
> > > 
> > > Maslovs Method in Dogelog Player 
> > > https://www.facebook.com/groups/dogelog

[toc] | [prev] | [next] | [standalone]

#12539

Some papers show calculi with two substitution rules
where the equation appears as ~(s=t) and flipped
as ~(t=s). Strange in our take we dont need this, 

only flipped polarity of atomic formulas, this
is provable with a=b in it:

1. a = b ∧ p(a) ⇒ p(b) 
2. p(b)   (T⇒2 1) 
3. ¬(a = b ∧ p(a))   (T⇒1 1) 
4. ¬p(a)   (F∧2 3) 
5. ¬a = b   (F∧1 3) 
6. ¬p(b)   (F= 5, 4)
    ✓   (ax 6, 2) 

And now with flipped b=a, it works as well:

1. b = a ∧ p(a) ⇒ p(b) 
2. p(b)   (T⇒2 1) 
3. ¬(b = a ∧ p(a))   (T⇒1 1) 
4. ¬p(a)   (F∧2 3) 
5. ¬b = a   (F∧1 3) 
6. p(a)   (F= 5, 2)
    ✓   (ax 4, 6)

See also:

First-Order Equality for Maslovs Method
https://twitter.com/dogelogch/status/1482885333486379015

First-Order Equality for Maslovs Method
https://www.facebook.com/groups/dogelog

[toc] | [prev] | [next] | [standalone]

#12542

I did the barber paradox always wrong!
The biconditional makes it so much easier.

1. ¬∃y ∀x (s(x, y) ⇔ ¬s(x, x))
2. ¬∀x (s(x, a) ⇔ ¬s(x, x))   (F∃ 1)
3. ¬(s(a, a) ⇔ ¬s(a, a))   (F∀ 2)
   4. ¬(s(a, a) ∧ ¬s(a, a))   (F⇔1 3)
   5. ¬¬s(a, a)   (F∧2 4)
   6. ¬s(a, a)   (F∧1 4)
   7. s(a, a)   (F¬ 5)
      ✓   (ax 6, 7)
4. s(a, a) ∨ ¬s(a, a)   (F⇔2 3)
   5. ¬s(a, a)   (T∨2 4)
   6. s(a, a)   (T∨1 4)
      ✓   (ax 5, 6)

See also:

Biconditional Support for Maslovs Method
https://twitter.com/dogelogch/status/1483455561031106563

Biconditional Support for Maslovs Method
https://www.facebook.com/groups/dogelog

[toc] | [prev] | [next] | [standalone]

#12543

Its a pitty that there is no simple leanTap=, i.e. leanTap= with 
equality. My take is only a few lines, splitting (subst) into (subst1) 
and (subst2) and can run in the browser. 

On the other hand I read:

    The completion-based method for mixed E-unification we 
    have described, has been implemented as part of the 
    tableau-based theorem prover 3TAP [3]. The implementation 
    consists of about 2500 lines of code, written in Quintus Prolog.
    Besides the possibility to prove theorems from predicate logic 
    with equality, the E-unification module can be used “stand alone” 
    to solve simultaneous mixed E-unification problems.
    https://formal.kastel.kit.edu/beckert/pub/Mixed_Rigid_Universal_E_Unification_CADE94.pdf

I don’t know how to run 2500 lines of code in the browser. 
And I don’t need some first order equality that would even 
deploy some term order, as is popular in certain term 

rewriting and Knuth Bendix. One interesting test case is this 
one, that works in the browser:

?- time(prove0('∀x∀y∀z∀t f(x,y,z,t)=f(y,z,t,x)⇒\
f(a,b,c,d)=f(c,d,a,b)', 9, unicode)), !.
% Wall 60 ms, gc 0 ms, 1171000 lips

Thanks to McCarthys trick its quite fast. On monday it still took 
me around 5000 ms, but now its only 60 ms. Wolfgangs Schwartz 
tool can do the same, but interestingly he gets a longer proof with

more (subst) applications. See also this ticket:

Does the tree tool search shortest proofs? #11
https://github.com/wo/tpg/issues/11

Mostowski Collapse schrieb am Dienstag, 18. Januar 2022 um 16:57:38 UTC+1:
> I did the barber paradox always wrong! 
> The biconditional makes it so much easier. 
> 
> 1. ¬∃y ∀x (s(x, y) ⇔ ¬s(x, x)) 
> 2. ¬∀x (s(x, a) ⇔ ¬s(x, x)) (F∃ 1) 
> 3. ¬(s(a, a) ⇔ ¬s(a, a)) (F∀ 2) 
> 4. ¬(s(a, a) ∧ ¬s(a, a)) (F⇔1 3) 
> 5. ¬¬s(a, a) (F∧2 4) 
> 6. ¬s(a, a) (F∧1 4) 
> 7. s(a, a) (F¬ 5) 
> ✓ (ax 6, 7) 
> 4. s(a, a) ∨ ¬s(a, a) (F⇔2 3) 
> 5. ¬s(a, a) (T∨2 4) 
> 6. s(a, a) (T∨1 4) 
> ✓ (ax 5, 6) 
> 
> See also: 
> 
> Biconditional Support for Maslovs Method 
> https://twitter.com/dogelogch/status/1483455561031106563 
> 
> Biconditional Support for Maslovs Method 
> https://www.facebook.com/groups/dogelog

[toc] | [prev] | [next] | [standalone]

#12544

See also my blog post on medium.com:

McCarthys Trick for First Order Equality
https://twitter.com/dogelogch/status/1484032442717585409

McCarthys Trick for First Order Equality
https://www.facebook.com/groups/dogelog

Mostowski Collapse schrieb am Donnerstag, 20. Januar 2022 um 15:03:24 UTC+1:
> Its a pitty that there is no simple leanTap=, i.e. leanTap= with 
> equality. My take is only a few lines, splitting (subst) into (subst1) 
> and (subst2) and can run in the browser. 
> 
> On the other hand I read: 
> 
> The completion-based method for mixed E-unification we 
> have described, has been implemented as part of the 
> tableau-based theorem prover 3TAP [3]. The implementation 
> consists of about 2500 lines of code, written in Quintus Prolog. 
> Besides the possibility to prove theorems from predicate logic 
> with equality, the E-unification module can be used “stand alone” 
> to solve simultaneous mixed E-unification problems. 
> https://formal.kastel.kit.edu/beckert/pub/Mixed_Rigid_Universal_E_Unification_CADE94.pdf 
> 
> I don’t know how to run 2500 lines of code in the browser. 
> And I don’t need some first order equality that would even 
> deploy some term order, as is popular in certain term 
> 
> rewriting and Knuth Bendix. One interesting test case is this 
> one, that works in the browser: 
> 
> ?- time(prove0('∀x∀y∀z∀t f(x,y,z,t)=f(y,z,t,x)⇒\ 
> f(a,b,c,d)=f(c,d,a,b)', 9, unicode)), !. 
> % Wall 60 ms, gc 0 ms, 1171000 lips 
> 
> Thanks to McCarthys trick its quite fast. On monday it still took 
> me around 5000 ms, but now its only 60 ms. Wolfgangs Schwartz 
> tool can do the same, but interestingly he gets a longer proof with 
> 
> more (subst) applications. See also this ticket: 
> 
> Does the tree tool search shortest proofs? #11 
> https://github.com/wo/tpg/issues/11
> Mostowski Collapse schrieb am Dienstag, 18. Januar 2022 um 16:57:38 UTC+1: 
> > I did the barber paradox always wrong! 
> > The biconditional makes it so much easier. 
> > 
> > 1. ¬∃y ∀x (s(x, y) ⇔ ¬s(x, x)) 
> > 2. ¬∀x (s(x, a) ⇔ ¬s(x, x)) (F∃ 1) 
> > 3. ¬(s(a, a) ⇔ ¬s(a, a)) (F∀ 2) 
> > 4. ¬(s(a, a) ∧ ¬s(a, a)) (F⇔1 3) 
> > 5. ¬¬s(a, a) (F∧2 4) 
> > 6. ¬s(a, a) (F∧1 4) 
> > 7. s(a, a) (F¬ 5) 
> > ✓ (ax 6, 7) 
> > 4. s(a, a) ∨ ¬s(a, a) (F⇔2 3) 
> > 5. ¬s(a, a) (T∨2 4) 
> > 6. s(a, a) (T∨1 4) 
> > ✓ (ax 5, 6) 
> > 
> > See also: 
> > 
> > Biconditional Support for Maslovs Method 
> > https://twitter.com/dogelogch/status/1483455561031106563 
> > 
> > Biconditional Support for Maslovs Method 
> > https://www.facebook.com/groups/dogelog

[toc] | [prev] | [next] | [standalone]

#12548

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

Mostowski Collapse schrieb am Donnerstag, 20. Januar 2022 um 15:06:05 UTC+1:
> See also my blog post on medium.com: 
> 
> McCarthys Trick for First Order Equality 
> https://twitter.com/dogelogch/status/1484032442717585409 
> 
> McCarthys Trick for First Order Equality 
> https://www.facebook.com/groups/dogelog

[toc] | [prev] | [next] | [standalone]

#12552

This one is much shorter, 6 pages code by Triska, 2015:
Prolog implementation of the Knuth-Bendix completion procedure
https://www.metalevel.at/trs/

But is it lean? Something shorter maybe?

Mostowski Collapse schrieb am Donnerstag, 20. Januar 2022 um 15:03:24 UTC+1:
> The completion-based method for mixed E-unification we 
> have described, has been implemented as part of the 
> tableau-based theorem prover 3TAP [3]. The implementation 
> consists of about 2500 lines of code, written in Quintus Prolog. 
> Besides the possibility to prove theorems from predicate logic 
> with equality, the E-unification module can be used “stand alone” 
> to solve simultaneous mixed E-unification problems. 
> https://formal.kastel.kit.edu/beckert/pub/Mixed_Rigid_Universal_E_Unification_CADE94.pdf 

[toc] | [prev] | [next] | [standalone]

#12549

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

[toc] | [prev] | [next] | [standalone]

#12550

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

[toc] | [prev] | [next] | [standalone]

#12551

If I paste my poket McCarthy into Joseph Vidal-Rossets web
page, I can reproduce the example from page 7 of this paper:

leanTAP Revisited 
Melvin Fitting - March 13, 1997
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36.3518&rep=rep1&type=pdf

Simply use this here:
?- provable(((~p & q) | p), Proof).

The red color shows where the proof tree ends in Γ |- .
Joseph Vidal-Rosset could make a fork of his website, 
that provides poket McCarthy directly for experimentation, 

also using better proof tree lables. My own web site
does not yet show some red color. Thats a little too 
early. First need to get my head around model finding

from tableaux for the non-propositional case...

Mostowski Collapse schrieb am Sonntag, 23. Januar 2022 um 01:32:19 UTC+1:
> 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).

[toc] | [prev] | [next] | [standalone]

#12553

Melvin Fitting uses the anti-sequents in a semantic completeness
argument. This then explains how validity proving is relatated to SAT
solving. Actually to be precise, validity is UNSAT. For randomized

algorithms there are complexity results for (SAT, ε-UNSAT). But these
results only appeared in recent years.

Mostowski Collapse schrieb am Sonntag, 23. Januar 2022 um 16:54:35 UTC+1:
> If I paste my poket McCarthy into Joseph Vidal-Rossets web 
> page, I can reproduce the example from page 7 of this paper: 
> 
> leanTAP Revisited 
> Melvin Fitting - March 13, 1997 
> http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.36.3518&rep=rep1&type=pdf 
> 
> Simply use this here: 
> ?- provable(((~p & q) | p), Proof). 
> 
> The red color shows where the proof tree ends in Γ |- . 
> Joseph Vidal-Rosset could make a fork of his website, 
> that provides poket McCarthy directly for experimentation, 
> 
> also using better proof tree lables. My own web site 
> does not yet show some red color. Thats a little too 
> early. First need to get my head around model finding 
> 
> from tableaux for the non-propositional case...
> Mostowski Collapse schrieb am Sonntag, 23. Januar 2022 um 01:32:19 UTC+1: 
> > 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).

[toc] | [prev] | [next] | [standalone]

#12568

Today a little show of what can go wrong: Question 
was why does Jens Otten leanseq_v5.pl use this:

prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !,
                         copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
                         J1 is J+1,
                         prove(G > [A1|D1],FV,I,J1,K).

And not this:

prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !,
                         copy_term((X:A,FV),(f_sk(J):A1,FV)),
                         J1 is J+1,
                         prove(G > [A1|D1],FV,I,J1,K).

The offending test case is this here:

∀y∃xFxy → ∃z∀tFzt is invalid.
Countermodel:
Domain: { 0, 1 }
F: { (0,0), (1,1) }
https://www.umsu.de/trees/#~6y~7xFxy~5~7z~6tFzt

[toc] | [prev] | [next] | [standalone]

#12569

I guess there is some literature that explains everything. On the
other hand some Prolog experimentation could maybe help
increase intuition. leanseq_v5.pl first, and I get, limiting the 

depth to 10, it already takes quite some time with 10 in this 
automated prover which doesn’t have much optimizations:

% leanseq_v5.pl compiled 0.00 sec, 17 clauses
?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
iteration 1
iteration 2
iteration 3
iteration 4
iteration 5
iteration 6
iteration 7
iteration 8
iteration 9
iteration 10
false.

Now the faulty leanseq_v5f.pl, where the Skolem function
is replaced by only a Skolem constant:

% leanseq_v5f.pl compiled 0.00 sec, 17 clauses
?- prove((![Y]: ?[X]:p(X,Y) => ?[Z]:![T]:p(Z,T))).
iteration 1
iteration 2
true 

Mostowski Collapse schrieb am Sonntag, 30. Januar 2022 um 21:11:01 UTC+1:
> Today a little show of what can go wrong: Question 
> was why does Jens Otten leanseq_v5.pl use this: 
> 
> prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !, 
> copy_term((X:A,FV),(f_sk(J,FV):A1,FV)), 
> J1 is J+1, 
> prove(G > [A1|D1],FV,I,J1,K). 
> 
> And not this: 
> 
> prove(G > D,FV,I,J,K) :- select1((![X]:A),D,D1), !, 
> copy_term((X:A,FV),(f_sk(J):A1,FV)), 
> J1 is J+1, 
> prove(G > [A1|D1],FV,I,J1,K). 
> 
> The offending test case is this here: 
> 
> ∀y∃xFxy → ∃z∀tFzt is invalid. 
> Countermodel: 
> Domain: { 0, 1 } 
> F: { (0,0), (1,1) } 
> https://www.umsu.de/trees/#~6y~7xFxy~5~7z~6tFzt

[toc] | [prev] | [next] | [standalone]

Page 3 of 5 — ← Prev page 1 2 [3] 4 5  Next page →

Back to top | Article view | comp.lang.prolog

csiph-web