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 2 of 5 — ← Prev page 1 [2] 3 4 5  Next page →

#12440

But s(CAPS) could have some merits over lets say for example
negation as failure. Most likely s(CAPS) can be approached by
3-valued logic. There exist approaches to 3-valued logic where a

predicate p is split into p+ and p-. This would explain the ‘-Name’
in s(CASP). I made an interesting observation, this 3-valued logic is
possibly more monotonic than 2-valued logic with negation as failure.

Which then has impact on embedded implication. We are now talking
about logic programming and Prolog, and not anymore mathematical
logic. For example in this example here:

/* Negation as Failure Style */
?- (loaded => dead), dead.
true ;
false.

There is something non-monotonic going on. When I assume p in the
pressence of negation of failure I effectively assume p+ and retract p-. So
I am doing two things at once, the retract is a counter factual,

https://en.wikipedia.org/wiki/Counterfactual_conditional#Logic_and_semantics

I remove a fact. On the other hand adding embedded implication to s(CASP)
could lead to more monotonicity. This seen here. We could start with neither
p+ nor p- present, and this here has two monotonic movements by the

embedded implication:

/* s(CAPS) Style */ 
?- (loaded => dead), ('-loaded' => dead).
true ;
false.

Cool! 

Mostowski Collapse schrieb am Mittwoch, 10. November 2021 um 12:56:13 UTC+1:
> Was toying around with proof by cases, two versions 
> here of the Yale shooting problem: 
> 
> /* s(CAPS) Style */ 
> https://swish.swi-prolog.org/p/yale_shooting.pl 
> 
> /* Negation as Failure Style */ 
> https://swish.swi-prolog.org/p/yale_shooting2.pl 
> 
> Had to double check, wasn’t sure anymore about my 
> claims. Could be that I am already rusty. Yes if you add 
> proof by cases to intuitionistic logic, you get classical logic. 
> At last Wikipedia also says so: 
> 
> The system of classical logic is obtained by adding any one of the following axioms: 
> 
> ϕ ∨ ¬ ϕ (Law of the excluded middle. 
> May also be formulated as ( ϕ → χ ) → ( ( ¬ ϕ → χ ) → χ ).) 
> 
> https://en.wikipedia.org/wiki/Intuitionistic_logic#Relation_to_classical_logic 
> 
> Now (A → (B → C)) is the same as A & B → C, so an alternative 
> to the Law of excluded middle (LEM) is indeed proof by cases.

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

#12448

I tried this one now with s(CASP):

p(X,X).

q(X,Y) :- not p(X,Y).

?- ? q(X,Y).

And it gives me false. I was expecting dif(X,Y) instead.
Or what is the C in s(CASP)? C stands for constraints, right?

Edit 16.11.2021:
The original constructive negation paper (David Chan. 1988.
Constructive negation based on the completed database. In Proc. of ICLP-88.)
would at least require such an answer, since the completion of the fact p(X,X) is:

p(X,Y) <-> X = Y.

So when I call not p(X,Y), I basically call not X = Y, and the negation of unification
would be dif(X,Y) or somesuch. Can be expressed as constraint. The example
simple and doesn’t require quantifier elimination.

MiniKanren has recently tried to handle quantifiers:

Constructive Negation for MiniKanren
http://minikanren.org/workshop/2019/minikanren19-final4.pdf

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

#12449

Strange that the MiniKanren paper doesn’t mention Kunen, Negation in
logic programming from 1987, where decidability of such constraint
problems was posited.

Mostowski Collapse schrieb am Dienstag, 16. November 2021 um 03:46:51 UTC+1:
> I tried this one now with s(CASP): 
> 
> p(X,X). 
> 
> q(X,Y) :- not p(X,Y). 
> 
> ?- ? q(X,Y). 
> 
> And it gives me false. I was expecting dif(X,Y) instead. 
> Or what is the C in s(CASP)? C stands for constraints, right? 
> 
> Edit 16.11.2021: 
> The original constructive negation paper (David Chan. 1988. 
> Constructive negation based on the completed database. In Proc. of ICLP-88.) 
> would at least require such an answer, since the completion of the fact p(X,X) is: 
> 
> p(X,Y) <-> X = Y. 
> 
> So when I call not p(X,Y), I basically call not X = Y, and the negation of unification 
> would be dif(X,Y) or somesuch. Can be expressed as constraint. The example 
> simple and doesn’t require quantifier elimination. 
> 
> MiniKanren has recently tried to handle quantifiers: 
> 
> Constructive Negation for MiniKanren 
> http://minikanren.org/workshop/2019/minikanren19-final4.pdf

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

#12479

Looks like Corona had people exploring SWISH.

Looks like Robert Kowalski is also into the business with
some s(CASP) variant. In his new paper he also references
a former project PENG-ASP, but this had one of the classical

ASP solvers underneath. Maybe there are more test cases
than only the test case I presented to figure out what s(CASP)
is doing. But his system emphasis natural language, is baptized

LE, and the characterization is a little vague. My idea that it does
also do abduction might be totally wrong. It could be even the
case that the example they show “query one with scenario two”,

is in fact embedded implication, “scenario two” => “query one”:

    But, different from ACE and PENG, which are syntactic sugar 
    for first-order logic, LE is syntactic sugar for a variant of pure 
    Prolog, which is a non-monotonic, meta (or higher-order) logic. 
    The relationship of LE to this variant of Prolog is similar to the 
    relationship of PENG-ASP to the LP language ASP.
    Logical English for Legal Applications
    November 2021 - Robert Kowalski, Miguel Calejo and Jacinto Dávila
    https://www.researchgate.net/publication/356287669

Pure Prolog and non-monotonic is a little in contradiction? :astonished:
Yes and No. The Clark Completion is non-monotonic.

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

#12480

This shows me that functional programming is on the decline:

Google Trends: Logic vs Functional Programming - From 2004 to 2021
https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming

I wonder whether this will have an impact on proof assistants.
Some of them have clearly a functional programming inclining.

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

#12481

This is also an interesting article, mentioning a new
trend such as "Multiparadigm languages":

Where Programming, Ops, AI, and the Cloud are Headed in 2021
https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/

We just observed that Python 3.10 introduced a new 
pattern matching construct. Now there is a  proposal 
for Java JDK 17 followup for some pattern matching 
like switch statement. I guess there is an unspoken law:

"Every programming language over the long
run will evolve into some Prolog variant"

Well this is too harsh, maybe this pattern matching only 
mimicks Haskell single sided unification and not Prolog 
unification. But what if people get fed up 
with single sided unification?

LoL

Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1:
> This shows me that functional programming is on the decline: 
> 
> Google Trends: Logic vs Functional Programming - From 2004 to 2021 
> https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming 
> 
> I wonder whether this will have an impact on proof assistants. 
> Some of them have clearly a functional programming inclining.

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

#12482

Maybe the assumption that programming language further
evolve is wrong, they could also devolve to assembler again?

Awaken In 2505, Humans Devolve
https://www.youtube.com/watch?v=mnLxc954ipo

At least this would truely help to have full control of 
the performance and memory allocation of your code.

LMAO!

Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:29:16 UTC+1:
> This is also an interesting article, mentioning a new 
> trend such as "Multiparadigm languages": 
> 
> Where Programming, Ops, AI, and the Cloud are Headed in 2021 
> https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/ 
> 
> We just observed that Python 3.10 introduced a new 
> pattern matching construct. Now there is a proposal 
> for Java JDK 17 followup for some pattern matching 
> like switch statement. I guess there is an unspoken law: 
> 
> "Every programming language over the long 
> run will evolve into some Prolog variant" 
> 
> Well this is too harsh, maybe this pattern matching only 
> mimicks Haskell single sided unification and not Prolog 
> unification. But what if people get fed up 
> with single sided unification? 
> 
> LoL
> Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1: 
> > This shows me that functional programming is on the decline: 
> > 
> > Google Trends: Logic vs Functional Programming - From 2004 to 2021 
> > https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming 
> > 
> > I wonder whether this will have an impact on proof assistants. 
> > Some of them have clearly a functional programming inclining.

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

#12483

There was a proposal:
https://area51.stackexchange.com/proposals/29144/beginner-theoretical-computer-science
But it now says:
This proposal has been deleted

Now if you want to join cstheory.stackexchange.com it
says Anybody can ask a question Anybody can answer
The best answers are voted up and rise to the top

But if you do that, they slap their policy into your face:
It allows only questions that "can be discussed between
two professors or between two graduate students working
on Ph.D.'s, but not usually between a professor and a
typical undergraduate student".
https://meta.stackexchange.com/questions/79351/should-research-level-only-sites-be-allowed

I am not lying when I say even Andrej Bauer did
that. But how do you want to launch a proof assistants
site, I assume for everybody? if you cannot divert
cs theory questions to another stackexchange?

proof assistants are full of cs theory stuff. 

Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 20:31:11 UTC+1:
> Maybe the assumption that programming language further 
> evolve is wrong, they could also devolve to assembler again? 
> 
> Awaken In 2505, Humans Devolve 
> https://www.youtube.com/watch?v=mnLxc954ipo 
> 
> At least this would truely help to have full control of 
> the performance and memory allocation of your code. 
> 
> LMAO!
> Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:29:16 UTC+1: 
> > This is also an interesting article, mentioning a new 
> > trend such as "Multiparadigm languages": 
> > 
> > Where Programming, Ops, AI, and the Cloud are Headed in 2021 
> > https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/ 
> > 
> > We just observed that Python 3.10 introduced a new 
> > pattern matching construct. Now there is a proposal 
> > for Java JDK 17 followup for some pattern matching 
> > like switch statement. I guess there is an unspoken law: 
> > 
> > "Every programming language over the long 
> > run will evolve into some Prolog variant" 
> > 
> > Well this is too harsh, maybe this pattern matching only 
> > mimicks Haskell single sided unification and not Prolog 
> > unification. But what if people get fed up 
> > with single sided unification? 
> > 
> > LoL 
> > Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1: 
> > > This shows me that functional programming is on the decline: 
> > > 
> > > Google Trends: Logic vs Functional Programming - From 2004 to 2021 
> > > https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming 
> > > 
> > > I wonder whether this will have an impact on proof assistants. 
> > > Some of them have clearly a functional programming inclining.

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

#12484

Anyway, these bitrot exchanges are mushrooming,
what about this one, would it be helpful?

https://cs.stackexchange.com/

Mostowski Collapse schrieb am Montag, 29. November 2021 um 00:20:32 UTC+1:
> There was a proposal: 
> https://area51.stackexchange.com/proposals/29144/beginner-theoretical-computer-science 
> But it now says: 
> This proposal has been deleted 
> 
> Now if you want to join cstheory.stackexchange.com it 
> says Anybody can ask a question Anybody can answer 
> The best answers are voted up and rise to the top 
> 
> But if you do that, they slap their policy into your face: 
> It allows only questions that "can be discussed between 
> two professors or between two graduate students working 
> on Ph.D.'s, but not usually between a professor and a 
> typical undergraduate student". 
> https://meta.stackexchange.com/questions/79351/should-research-level-only-sites-be-allowed 
> 
> I am not lying when I say even Andrej Bauer did 
> that. But how do you want to launch a proof assistants 
> site, I assume for everybody? if you cannot divert 
> cs theory questions to another stackexchange? 
> 
> proof assistants are full of cs theory stuff.
> Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 20:31:11 UTC+1: 
> > Maybe the assumption that programming language further 
> > evolve is wrong, they could also devolve to assembler again? 
> > 
> > Awaken In 2505, Humans Devolve 
> > https://www.youtube.com/watch?v=mnLxc954ipo 
> > 
> > At least this would truely help to have full control of 
> > the performance and memory allocation of your code. 
> > 
> > LMAO! 
> > Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:29:16 UTC+1: 
> > > This is also an interesting article, mentioning a new 
> > > trend such as "Multiparadigm languages": 
> > > 
> > > Where Programming, Ops, AI, and the Cloud are Headed in 2021 
> > > https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/ 
> > > 
> > > We just observed that Python 3.10 introduced a new 
> > > pattern matching construct. Now there is a proposal 
> > > for Java JDK 17 followup for some pattern matching 
> > > like switch statement. I guess there is an unspoken law: 
> > > 
> > > "Every programming language over the long 
> > > run will evolve into some Prolog variant" 
> > > 
> > > Well this is too harsh, maybe this pattern matching only 
> > > mimicks Haskell single sided unification and not Prolog 
> > > unification. But what if people get fed up 
> > > with single sided unification? 
> > > 
> > > LoL 
> > > Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1: 
> > > > This shows me that functional programming is on the decline: 
> > > > 
> > > > Google Trends: Logic vs Functional Programming - From 2004 to 2021 
> > > > https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming 
> > > > 
> > > > I wonder whether this will have an impact on proof assistants. 
> > > > Some of them have clearly a functional programming inclining.

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

#12488

The devolution could be also a form of evolution. I recently saw
a book about ARM assembly which had a garbage collection
section. In 2018 ARM started supporting pointer tagging.

See also:

ARM Memory Tagging Extension
Kosty Serbryany - 2019
https://www.usenix.org/system/files/login/articles/login_summer19_03_serebryany.pdf

C–: a portable assembly language that supports garbage collection
Simon Peyton Jones - 1999
https://www.cs.tufts.edu/~nr/pubs/c–gc.pdf

Basically what was once conceived as a Java Chip seems to
happen right now. You can also view it as LISP on a Chip I guess,
remove the object oriented obsession, and focus on safety.

Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 20:31:11 UTC+1:
> Maybe the assumption that programming language further 
> evolve is wrong, they could also devolve to assembler again? 
> 
> Awaken In 2505, Humans Devolve 
> https://www.youtube.com/watch?v=mnLxc954ipo 
> 
> At least this would truely help to have full control of 
> the performance and memory allocation of your code. 
> 
> LMAO!
> Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:29:16 UTC+1: 
> > This is also an interesting article, mentioning a new 
> > trend such as "Multiparadigm languages": 
> > 
> > Where Programming, Ops, AI, and the Cloud are Headed in 2021 
> > https://www.oreilly.com/radar/where-programming-ops-ai-and-the-cloud-are-headed-in-2021/ 
> > 
> > We just observed that Python 3.10 introduced a new 
> > pattern matching construct. Now there is a proposal 
> > for Java JDK 17 followup for some pattern matching 
> > like switch statement. I guess there is an unspoken law: 
> > 
> > "Every programming language over the long 
> > run will evolve into some Prolog variant" 
> > 
> > Well this is too harsh, maybe this pattern matching only 
> > mimicks Haskell single sided unification and not Prolog 
> > unification. But what if people get fed up 
> > with single sided unification? 
> > 
> > LoL 
> > Mostowski Collapse schrieb am Sonntag, 28. November 2021 um 16:22:27 UTC+1: 
> > > This shows me that functional programming is on the decline: 
> > > 
> > > Google Trends: Logic vs Functional Programming - From 2004 to 2021 
> > > https://trends.google.de/trends/explore?date=all&q=logic%20programming,functional%20programming 
> > > 
> > > I wonder whether this will have an impact on proof assistants. 
> > > Some of them have clearly a functional programming inclining.

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

#12504

What about this riddle, doing it in Prolog, s(CASP) or LK?
(LK as per the Phil Zucker page might not do it,
would need a FOL or so extension I guess)

An impossible asylum - Avigad et al. 2021
“In 1982, Raymond Smullyan published an article, “The Asylum of
Doctor Tarr and Professor Fether,” that consists of a series of
puzzles. These were later reprinted in the anthology, “The Lady
or The Tiger? and Other Logic Puzzles.” The last puzzle, which
describes the asylum alluded to in the title, was designed to be
especially difficult. With the help of automated reasoning, we
show that the puzzle’s hypotheses are, in fact, inconsistent,
which is to say, no such asylum can possibly exist.”
https://arxiv.org/abs/2112.02142

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

#12507

No Son of BirdBrain III yet in sight? 
I tried https://www.umsu.de/trees/ on this here, to find a model of:

E * x = x. % left identity
x’ * x = E. % left inverse
(x * y) * z = x * (y * z). % associativity
A * B != B * A. % A and B do not commute

But its horribly choking.

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

#12509

Interesting call:

"For example, have a look at the Coq standard libarary or
the user contributions, these are formalizations of
mathematics in type theory. And this stuff is written mostly
by computer scientists. If mathematicians moved onto
the proof-assistant bandwagon, there would be much more."
https://mathoverflow.net/a/133599

Maybe they would join the bandwagon if there were
less typos? Whats a "libarary"? Is it library? Or libarray?

LoL 

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

#12510

Small bug in the LK code:

There is a nice theorem prover for propositional logic with LK implemented in Prolog here:
https://www.philipzucker.com/javascript-automated-proving/

Its not complete for FOL matrices, try this:

prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof). 
Failed To Prove.

Now remove the cut in the axiom rule:

prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof). 
X = s

Mostowski Collapse schrieb am Dienstag, 28. Dezember 2021 um 19:26:21 UTC+1:
> Interesting call: 
> 
> "For example, have a look at the Coq standard libarary or 
> the user contributions, these are formalizations of 
> mathematics in type theory. And this stuff is written mostly 
> by computer scientists. If mathematicians moved onto 
> the proof-assistant bandwagon, there would be much more." 
> https://mathoverflow.net/a/133599 
> 
> Maybe they would join the bandwagon if there were 
> less typos? Whats a "libarary"? Is it library? Or libarray? 
> 
> LoL

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

#12511

To handle FOL matrices, unify_with_occurs_check/2 might
also come into play. Whats a short example and short
explanation about things that can go wrong?

Mostowski Collapse schrieb:
> Small bug in the LK code:
> 
> There is a nice theorem prover for propositional logic with LK implemented in Prolog here:
> https://www.philipzucker.com/javascript-automated-proving/
> 
> Its not complete for FOL matrices, try this:
> 
> prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
> Failed To Prove.
> 
> Now remove the cut in the axiom rule:
> 
> prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof).
> X = s
> 
> Mostowski Collapse schrieb am Dienstag, 28. Dezember 2021 um 19:26:21 UTC+1:
>> Interesting call:
>>
>> "For example, have a look at the Coq standard libarary or
>> the user contributions, these are formalizations of
>> mathematics in type theory. And this stuff is written mostly
>> by computer scientists. If mathematicians moved onto
>> the proof-assistant bandwagon, there would be much more."
>> https://mathoverflow.net/a/133599
>>
>> Maybe they would join the bandwagon if there were
>> less typos? Whats a "libarary"? Is it library? Or libarray?
>>
>> LoL

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

#12512

Oh, this is very nice!

∃x∃y(Pyy → Pxf(x)) is invalid.
https://www.umsu.de/trees/#~7x~7y%28Pyy~5Pxf%28x%29%29

Countermodel:
Domain: 	{ 0, 1 }
f: 	{ (0,1), (1,0) }
P: 	{ (0,0), (1,1) }

Mostowski Collapse schrieb am Donnerstag, 30. Dezember 2021 um 09:56:23 UTC+1:
> To handle FOL matrices, unify_with_occurs_check/2 might 
> also come into play. Whats a short example and short 
> explanation about things that can go wrong? 
> 
> Mostowski Collapse schrieb:
> > Small bug in the LK code: 
> > 
> > There is a nice theorem prover for propositional logic with LK implemented in Prolog here: 
> > https://www.philipzucker.com/javascript-automated-proving/ 
> > 
> > Its not complete for FOL matrices, try this: 
> > 
> > prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof). 
> > Failed To Prove. 
> > 
> > Now remove the cut in the axiom rule: 
> > 
> > prove0(((p(X) => p(t) | p(s)) & (p(X) => p(s))), Proof). 
> > X = s 
> > 
> > Mostowski Collapse schrieb am Dienstag, 28. Dezember 2021 um 19:26:21 UTC+1: 
> >> Interesting call: 
> >> 
> >> "For example, have a look at the Coq standard libarary or 
> >> the user contributions, these are formalizations of 
> >> mathematics in type theory. And this stuff is written mostly 
> >> by computer scientists. If mathematicians moved onto 
> >> the proof-assistant bandwagon, there would be much more." 
> >> https://mathoverflow.net/a/133599 
> >> 
> >> Maybe they would join the bandwagon if there were 
> >> less typos? Whats a "libarary"? Is it library? Or libarray? 
> >> 
> >> LoL

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

#12513

On Thursday, 30 December 2021 at 10:06:49 UTC+1, burs...@gmail.com wrote:

> Oh, this is very nice! 

There is nothing nice about a fucking retard and piece of spamming
shit polluting all public ponds, you shameless retarded piece of shit.

But all I'd still want to know is who's the criminal nazi cunts who pay your bills...

*Plonk*

Julio

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

#12514

LoL, are you feeling tense Culio?

Julio Di Egidio <julio@diegidio.name> schrieb am Donnerstag, 30. Dezember 2021 um 11:48:09 UTC+1:
> On Thursday, 30 December 2021 at 10:06:49 UTC+1, burs...@gmail.com wrote: 
> 
> > Oh, this is very nice!
> There is nothing nice about a fucking retard and piece of spamming 
> shit polluting all public ponds, you shameless retarded piece of shit. 
> 
> But all I'd still want to know is who's the criminal nazi cunts who pay your bills... 
> 
> *Plonk* 
> 
> Julio

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

#12515

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]

#12516

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]

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

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

csiph-web