Welcome to novaBBS (click a section below) |
mail files register nodelist faq login |

Posted: 16 Hours 56 Minutes ago by: Aleksy Grabowski Hello, Why you didn't decide to use more classic dirname and basename? Meaning would've been immediately obvious for any experienced programmer. Best Regards, Alex On 5/24/22 12:43, Mostowski Collapse wrote: |

Posted: 1 Day 1 Hour ago by: Mostowski Collapse ?- sys_file_parent('/mnt/c/foo/bar/baz.p', X). X = '/mnt/c/foo/bar/'. ?- sys_file_name('C:/foo/bar/baz.p', X). X = 'baz.p'. ?- sys_file_parent('C:\\foo\\bar\\baz.p', X). X = 'C:\\foo\\bar\\'. ?- sys_file_name('C:\\foo\\bar\\baz.p', X). |

Posted: 1 Day 2 Hours ago by: Mostowski Collapse Here is a use case for last_sub_atom/5. Its useful to make an OS polyglott Prolog system, at least polyglott among Unix, Windows and Mac. You can get rid of Logtalks internal_os_path/2, which I think is a little design flaw in my old Prol |

Posted: 1 Day 2 Hours ago by: Mostowski Collapse Here from ISO core standard: ?- sub_atom('baaab', X, Y, Z, 'aa'). X = 1, Y = 2, Z = 2; X = 2, Y = 2, Z = 1; fail. ?- sub_atom('abracadabra', X, Y, Z, 'abra'). X = 0, Y = 4, Z = 7; X = 7, Y = 4, Z = 0. And here the analogue searching ba |

Posted: 1 Day 2 Hours ago by: Mostowski Collapse /* WSL */ ?- absolute_file_name('baz.p', X). X = '/mnt/c/foo/bar/baz.p' /* Windows 10 */ ?- absolute_file_name('baz.p', X). X = 'C:\\foo\\bar\\baz.p' So what to do? Normalize it and always use '/' and eliminate '\\' ? This is what I did |

Posted: 3 Days 14 Hours ago by: Mostowski Collapse Phylogenetic Trees for Prolog Operator Parsers https://twitter.com/dogelogch/status/1528118780890603522 Phylogenetic Trees for Prolog Operator Parsers https://www.facebook.com/groups/dogelog Mostowski Collapse schrieb am Samstag, 21. Ma |

Posted: 3 Days 23 Hours ago by: Mostowski Collapse And my suspicion got confirmed, Scryer and GNU do the same in fuzz4 test cases, except for a few amusing strange results: $ target/release/scryer-prolog -v "v0.9.0-146-g25418db2-modified" $ target/release/scryer-prolog ?- X = (- ( ( ) =: |

Posted: 3 Days 23 Hours ago by: Mostowski Collapse I made a kind of phylogenetic tree, the numbers in it indicate how many test cases the various Prolog systems agree. The results for fuzz4 are as follows: ?- pairing([eclipse4,gnu4,jekejeke4,swi4,scryer4,sicstus4, ppeg4,trealla4], |

Posted: 6 Days 12 Hours ago by: Richard Damon So, how do you use the meaning of the words in "The Square of the Hypotonuse of a right triangle is equal to the sume of the squares of the other two sides" to show it is true? I think you will have problems. |

Posted: 6 Days 21 Hours ago by: olcott “Analytic” sentences, such as “Pediatricians are doctors,” have historically been characterized as ones that are true by virtue of the meanings of their words alone and/or can be known to be so solely by knowing those meanings. |

Posted: 7 Days 1 Hour ago by: Richard Damon Absolutely NOT. There does NOT need to be proof that something is true. IF you want to claim that, by YOUR definition, you need to actually PROVE it. And, you can't do that by assuming it, you need to actually PROVE it from the accept |

Posted: 7 Days 1 Hour ago by: Mostowski Collapse Now I have a new project going. I need a better microscope to find differences in parsing of the different Prolog systems. So that I might generate a phylogenic tree. I see a trend against ECliPSe Prolog concering fuzz3, now also results |

Posted: 7 Days 9 Hours ago by: olcott Unless and Until a (possibly unknown) connection exists between an expression of language back-chained by sound deductive inference steps to known truth, the expression is not true. None-the-less the sequence of inference steps must e |

Posted: 7 Days 14 Hours ago by: Mostowski Collapse $ target/release/scryer-prolog ?- X = foo = bar = baz = 'ab\qc' . error(syntax_error(invalid_single_quoted_character),read_term/3). Initially my thought was my monadic parser from Dogelog player will automatically be able to deal with |

Posted: 7 Days 14 Hours ago by: Mostowski Collapse My parser research has arrived at this eclectic challenge. Here is an example where I can coerce both SWI-Prolog and pPEG SWIPL Example into masking the real error. Here is what ECLiPSe Prolog does: [eclipse 1]: X = foo = bar = baz = ' |

Posted: 9 Days 7 Hours ago by: Markus Triska Frequently Asked Questions - comp.lang.prolog Last-modified: 2022-02-24 Last-changes: Update link to tutorial by J.R. Fisher. Geoffrey Churchill. Markus Triska (Mar. 2 2007 - ... ) Remko Troncon (Jan. 6 2002 - Mar |

Posted: 10 Days 1 Hour ago by: Richard Damon Which means it HAS a truth value of True or False but we don't know which. That is VERY difffernt then it having neither, which is what you have been claimiing (or at least what your words meant). This shows your confusion between Trut |

Posted: 10 Days 8 Hours ago by: olcott It can only be declared as having an unknown truth value. |

Posted: 10 Days 12 Hours ago by: Richard Damon Source for this "Claim". It can not be labeld "Analytically True", yes, but nothing says it can not be True. (If we can't prove it True we can not use it to actually directly prove something else, but it can be True). You seem to be sa |

Posted: 10 Days 13 Hours ago by: olcott We cannot correctly label any analytical expression of language as true unless and until: (1) It has been stipulated to be true. (2) a connected set of semantic meanings back-chain to expressions of language that have been stipulated t |

Posted: 10 Days 13 Hours ago by: Richard Damon So something can be "Provable" yet no "Proof" actually be findable or expressable? That means you might not know if you have Proven Something. So, again, your are at the wrong end. If you want to change the fundamental definitions, y |

Posted: 10 Days 14 Hours ago by: olcott So this is where correct reasoning and logic diverge on terminology. When I refer to a set of connected semantic meanings this seems not exactly the same thing as a proof. If this set does not exist, then the expression is not true. If |

Posted: 10 Days 15 Hours ago by: Richard Damon FALSE. Where is the Collatz conjecture being True in that? (If it is) Unless you make the finite sequence from axioms to the result, you don't have a Proof. Then why are you talking about fields of LOGIC? Formal Logic STARTS with it |

Posted: 10 Days 15 Hours ago by: olcott OK great this is a key agreement between us. Analytically True or False is the same as True or False, except that is excludes expressions of language dealing with sense data from the sense organs. If it is true then there must be a |

Posted: 10 Days 16 Hours ago by: Richard Damon Then stop talking about things that aren't analytically true. For instance, Godel's G is NOT 'Analytically True' in F, because you can't prove it, but it IS 'True' because you can show via a meta-logical proof in a higher system that i |

Posted: 10 Days 19 Hours ago by: olcott I am ALWAYS only talking about ANALYTIC TRUTH, the only time I ever talk about EMPIRICAL TRUTH, is to say that I am not talking about that. If the answer requires an infinite search then this answer cannot be derived in finite time. N |

Posted: 10 Days 19 Hours ago by: Richard Damon WRONG. Again you conflate Analytic truth with truth. The Collatz conjecture, that there exist no number N such that the sequence of progreesing to 3N+1 for N odd, and N/2 for N even doesn't eventually reach 1, MUST be either True of Fa |

Posted: 10 Days 20 Hours ago by: olcott No, I independently verified his reasoning before I ever saw his reasoning. That no counter-examples can possibly exist is complete proof that it is true. There are no categories of expressions of language that are both true and neith |

Posted: 11 Days 21 Hours ago by: Mostowski Collapse ATOM TOTAL FAILURE LoL Mostowski Collapse schrieb am Mittwoch, 21. Juli 2021 um 18:37:10 UTC+2: |

Posted: 12 Days 12 Hours ago by: Archimedes Plutonium Is ETH, Richard Pink, Tristan Riviere, Dietmar Salamon, as dumb and stupid as the math failure Jan Burse with his ellipse a conic when it is a oval. And no wonder no-one at ETH can ask the question with is the atom's true electron-- muon o |

Posted: 12 Days 22 Hours ago by: Mostowski Collapse / |_| o o He is quite happy. Mostowski Collapse schrieb: |

Posted: 13 Days 4 Hours ago by: Archimedes Plutonium Terence Tao,Paul Biran, Marc Burger, Patrick Cheridito, ETH Zurich On Saturday, June 9, 2018 at 6:35:36 PM UTC-5, Mostowski Collapse (Jan Burse) wrote: UCLA chancellor: Gene D. Block (biology) UCLA Physics dept Ernest Abers, Elihu Ab |

Posted: 13 Days 4 Hours ago by: Archimedes Plutonium Terence Tao,Paul Biran, Marc Burger, Patrick Cheridito, ETH Zurich On Saturday, June 9, 2018 at 6:35:36 PM UTC-5, Mostowski Collapse (Jan Burse) wrote: UCLA chancellor: Gene D. Block (biology) UCLA Physics dept Ernest Abers, Elihu Ab |

Posted: 13 Days 23 Hours ago by: Mostowski Collapse Why do you wanter the plants, when it rains? Mostowski Collapse schrieb am Mittwoch, 21. Juli 2021 um 18:37:10 UTC+2: |

Posted: 15 Days 15 Hours ago by: Mostowski Collapse Why do you wanter the plants, when it rains? Mostowski Collapse schrieb: |

Posted: 15 Days 19 Hours ago by: Archimedes Plutonium Dorothy E. Aronson,Miguel Cardona,Cindy Marten, Kibo says lost or stolen marbles Donald Schwendeman,Jeffrey Banks,Kristin Bennett,Rensselaer Polytechnic,Vincent Meunier, Ethan Brown, Glenn Ciolek, Julian S. Georg, Joel T. Giedt On Satur |

Posted: 17 Days 14 Hours ago by: olcott My H proves that H(P,P)== false on the basis that H does correctly compute the mapping from its input parameters to its own final reject state on the basis of the actual behavior actually specified by its input parameters. The details |

Posted: 18 Days 16 Hours ago by: olcott Gödel says that it does with dodgy words that also says that it does not. 15 In spite of appearances, there is nothing circular about such a proposition, since it begins by asserting the unprovability of a wholly determinate formula ( |

Posted: 19 Days ago by: Richard Damon Which is Godel making a comment about G, and not a statement in G itself. G does not directly mention itself in the Theory. So this comment of mine is now proven. And you have prooved to be a Liar and an idiot, as you abolutely don't |

Posted: 19 Days 5 Hours ago by: Paola Cattabriga At the time of my graduation thesis, many years ago, I used the highly appreciated volume of Chang and Lee, Symbolic Logic and Mechanical Theorem Proving. Lately I found myself picking it up again adapting it to my current research, in pa |

Posted: 19 Days 9 Hours ago by: olcott In Tarski's theory p <is> the formalized liar paradox. Gödel says: ....We are therefore confronted with a proposition which asserts its own unprovability. |

Posted: 19 Days 10 Hours ago by: Richard Damon How do you get that. In the Theory, you can't even tell that G references itself, but is just a statement about mathematics. No, because in the theory, G doesn't even reference itself, so it can't be self-contradictory. I think you |

Posted: 19 Days 15 Hours ago by: olcott From the quote below: We are therefore confronted with a proposition which asserts its own unprovability. Gödel says: The analogy between this result and Richard’s antinomy leaps to the eye; there is also a close relationship with |

Posted: 19 Days 18 Hours ago by: André G. Isaak G is not self-contradictory in either the theory or the meta-theory. The Liar Paradox and G are not the same sentence. You keep treating them as if they were based solely on Gödel's claim that there is a close relationship between th |

Posted: 19 Days 18 Hours ago by: olcott Yes. Not at all. In the theory p is self-contradictory thus not a truth bearer. In the meta-theory p is NOT self-contradictory. G is self-contradictory on the theory and non self-contradictory in the meta-theory. |

Posted: 20 Days ago by: Richard Damon Nope, shows you don't understand the proof. Have you actually read it, or just the 'cliff notes' version. You know, the one with the actual Except that G isn't self-contradictory. The actual G makes a statement of a mathematical probl |

Posted: 20 Days 1 Hour ago by: Mostowski Collapse Ok, the aspiring academic Prolog idiot might want to know more. But from PEG context it should be clear, that this is the declarative reading for parsing, i.e. mode p(+,-). Not sure whether it is suitable for other modes. Didn't use it |

Posted: 20 Days 1 Hour ago by: Mostowski Collapse p(A, B) :- \+ q(A, _), A = C, r(C, B). The declarative reading is as follows: p(A, B) ← ¬ ∃D q(A, D) ∧ A = C ∧ r(C, B). Its not really rocket science. But because its negation as failure you might also need |

Posted: 20 Days 2 Hours ago by: Mostowski Collapse Looks like UWN is confusing GitHub with Facebook, with his up votes. And sometimes UWN thinks its YouTube, with his down votes? Mostowski Collapse schrieb am Donnerstag, 5. Mai 2022 um 12:08:16 UTC+2: |

Posted: 20 Days 2 Hours ago by: Mostowski Collapse The not-predicate expression !e succeeds if e fails and fails if e succeeds, again consuming no input in either case. Mostowski Collapse schrieb am Donnerstag, 5. Mai 2022 um 12:04:07 UTC+2: |

Posted: 20 Days 2 Hours ago by: Mostowski Collapse https://stackoverflow.com/questions/12758567/legitimate-uses-of-1 The question has two former answers from me. Stackoverflow didn't allow me to delete them. Nobody else has answered, and you are asking the wrong question. I find that ECL |

Posted: 20 Days 4 Hours ago by: Mostowski Collapse Maybe the phrase/3 translation grows out of the desire to a) make the translation not cut transparent, b) make the translation similar to the translation of ordinary (\+)/1 which does lazy body conversion for the meta variables in its arg |

Posted: 20 Days 4 Hours ago by: Mostowski Collapse The SWI-Prolog behaviour is the steadfast one. Mostowski Collapse schrieb am Donnerstag, 5. Mai 2022 um 09:52:29 UTC+2: |

Posted: 20 Days 4 Hours ago by: Mostowski Collapse At least UWNs translation would be steadfast. Here you see what is the difference between a steadfast, and a non-steadfast translation: Was running this test case: In Tau Prolog 0.3.2 (beta) I get: p([a],[]). false. On the other hand |

Posted: 20 Days 4 Hours ago by: Mostowski Collapse ?- listing. It then gives: p(A, B) :- \+ q(A, _), A = C, r(C, B). No singleton warning. And recently a little better listing with multiline pretty printing. |

Posted: 20 Days 5 Hours ago by: Mostowski Collapse So I heard it through the grape wine, Scryer Prolog does not have DCG (\+)/1. Dang! So far ECLiPSe Prolog, SWI-Prolog, GNU Prolog, SICStus Prolog have it. Why is this so? UWNs code doesn't make any sense: dcg_cbody(\+ GRBody, S0, S, ( \ |

Posted: 20 Days 9 Hours ago by: olcott In the same way that having a cat in your attic is proof that your car is leaking oil. It really has never made any sense how people can't understand that self-contradictory expressions of language are necessary semantically invalid. |

Posted: 20 Days 9 Hours ago by: Richard Damon So we can prove G in the Metatheory, so it is True in the Theory too. But if G is true in the Theory, it is BY DEFINITION not provable in the Theory, so the space of the Theory is shown to have a True Statement which is not provable, |

Posted: 20 Days 10 Hours ago by: olcott Tarski's hierarchy of languages. It only works at a higher level language because the expression of language at the next level is not self-contradictory. All epistemological antinomies are self-contradictory making them semantically i |

Posted: 20 Days 12 Hours ago by: Richard Damon No, because it doesn't meet the requirements to be a φ As you have mentioned elsewhere, the statement of the Liar Paradox isn't a Truth Beared, which is part of the requirements built into what φ needs to be. Note, your statement of |

Posted: 20 Days 17 Hours ago by: olcott LP exactly meets the mathematical definition of incompleteness, this will not be clear until after I correctly formalize it and specify the formal system to which it belongs. Tarski seems to provide the best head start on formalizing t |

Posted: 20 Days 17 Hours ago by: Mostowski Collapse Woa! A moment of silence for Scryer Prolog. It has become irreversibly unuseable, even basic Prolog logic doesn't work anymore... What the heck are they doing? Tons of unification and char list tickets on GitHub. But elementary things like |

Posted: 20 Days 22 Hours ago by: André G. Isaak How exactly does it 'plug right into the above'? As I just said, LP *is* provable. ¬LP is also provable. That's what it means to be a contradiction. André |

Posted: 21 Days 1 Hour ago by: Richard Damon Your fundamental error! Unless the system has define Truth to require provable, which mathematics hasn't, this is an error, as it isn't a fundamental error. There are many things that we know have a truth value, but are not provable o |

Posted: 21 Days 6 Hours ago by: olcott Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)). The Liar Paradox plugs right in to this making it equivalent to Gödel's G. |

Posted: 21 Days 8 Hours ago by: André G. Isaak Actually, it doesn't matter whether it is true or false. What's relevant here is that it is trivially easy to prove The Liar using a simple reductio ad absurdum. Unfortunately, it is equally trivially easy to prove ¬(The Liar) using a |

Posted: 21 Days 8 Hours ago by: André G. Isaak Neither 'impossibly true' nor 'impossibly false' are meaningful English. I really wish you would stop using this adverb as if it somehow made sense. It doesn't. G is definitely a truth bearer. It states that a specific polynomial equa |

Posted: 21 Days 8 Hours ago by: olcott No the LP is semantically incorrect. Someone here (I think its Andre) now seems to understand that if G is not provable in F then it is not true in F. If G is true it can only be true in an other different formal system than F. Tarski |

Posted: 21 Days 9 Hours ago by: olcott That if correct. If is is impossibly true or false then it is not a truth bearer. unprovable in the system entails untrue in the system. Sure, yet it is only true in this system which also makes it provable in that system. It can' |

Posted: 21 Days 9 Hours ago by: Richard Damon Your missing that he is meaning that if the Liar is TRUE, it shows the logic system to be inconsistent. While G being true just proves that the system is Incomplete. (G not being False in a system shows that the system is Inconsistent, |

Posted: 21 Days 9 Hours ago by: olcott Not according to the mathematical definition of incompleteness Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)). Anything and everything that is neither provable nor refutable in some formal system proves that this formal system IS |

Posted: 21 Days 14 Hours ago by: olcott In other words you have no rebuttal either because what I said is over your head or you want to make sure to never agree that I correctly proved my point. I vote for both. |

Posted: 21 Days 14 Hours ago by: Jeff Barnett T24gNS8zLzIwMjIgMToxMiBQTSwgb2xjb3R0IHdyb3RlOg0KPiBPbiA1LzMvMjAyMiAxOjMz IFBNLCBKZWZmIEJhcm5ldHQgd3JvdGU6DQo+PiBPbiA1LzMvMjAyMiA5OjE4IEFNLCBBbmRy w6kgRy4gSXNhYWsgd3JvdGU6DQo+Pj4gT24gMjAyMi0wNS0wMiAxODo1Nywgb2xjb3R0IHdy b3RlOg0KPj4NCj4+IElES |

Posted: 21 Days 16 Hours ago by: André G. Isaak But calling it a "non-truth bearer" simply because it has not been determined to be true would equally be an error. And it can be shown (i.e. correctly determined) that G is true, just not within the system for which it was constructed |

Posted: 21 Days 17 Hours ago by: André G. Isaak G is not a formalization of The Liar. There is no such formalization in the systems Gödel considers. The Liar results in inconsistency whereas G results in incompleteness. This is a major difference between G and The Liar which is wh |

Posted: 21 Days 17 Hours ago by: olcott Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)). I used the above as the precise measure of isomorphism. The whole error of the incompleteness theorem is entirely anchored in that the official mathematical definition of incomplete |

Posted: 21 Days 17 Hours ago by: olcott Yes that seems to be correct. On the other hand calling an expression of language true that has not be 'Correctly determined to be true' is an error. If G is claimed to be true then this assertion must be supported by: 'Correctly deter |

Posted: 21 Days 17 Hours ago by: Jeff Barnett T24gNS8zLzIwMjIgOToxOCBBTSwgQW5kcsOpIEcuIElzYWFrIHdyb3RlOg0KPiBPbiAyMDIy LTA1LTAyIDE4OjU3LCBvbGNvdHQgd3JvdGU6DQoNCklESU9UIFNOSVBQRUQNCg0KDQo+IE5v LiBUaGUgTGlhciBjYW4gYmUgdXNlZCB0byBjb25zdHJ1Y3QgYW4gKmlkZW50aWNhbCogcHJv b2YuIE90aGVyIA0KPiBhb |

Posted: 21 Days 18 Hours ago by: André G. Isaak <snippage> 'True' and 'Correctly determined to be true' mean different things. These are YOUR assumptions. They have not been demonstrated. And they are not consistent with the way in which the rest of the world talks about truth. Y |

Posted: 21 Days 18 Hours ago by: olcott OK. This is not any mere assumption. The only way that any analytic expressions of language are correctly determined to be true is: (a) They are defined to be true. (b) They are derived from applying truth preserving operations to (a) |

Posted: 21 Days 19 Hours ago by: André G. Isaak It is defined directly above. Trying reading more carefully. Here you're simply begging the question by assuming your own conclusion: that being true and being provable are the same. The whole point of Gödel's proof is that they cann |

Posted: 21 Days 19 Hours ago by: olcott OK, then I am very happy to say that my accusation that you lied was not justified, we were simply talking past each other. |

Posted: 21 Days 19 Hours ago by: olcott I have no idea what you mean by G-Prime. Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)). It is the fact that the mathematical definition of Incompleteness simply assumes that φ is semantically correct that is the core mistake o |

Posted: 21 Days 19 Hours ago by: André G. Isaak Of course really. His original proof drew on The Liar for inspiration. So a proof which draws on The Liar would be the same proof. He is saying that he could have used ANY antinomy. IOW, he could have chosen a *different* antinomy fro |

Posted: 21 Days 20 Hours ago by: olcott Really? That you persisted (six times) on claiming that Gödel's statement about the Liar Paradox overrode and superseded his statement about the entire category that the Liar Paradox belongs to was despicably deceitful, unless you b |

Posted: 21 Days 21 Hours ago by: André G. Isaak No. The Liar can be used to construct an *identical* proof. Other antinomies could be used for similar proofs. He's already talking about The Liar. You have some serious reading comprehension problems. I never denied the things Göde |

Posted: 21 Days 21 Hours ago by: Ben You are not a math guy. I am. No. G is provable. Though I did make a mistake -- the link was to a proof of G-RIT not G. How are you getting on with E and specifying P? Have you given up? |

Posted: 22 Days ago by: Richard Damon No, G IS provable, just not in the system F that G is described in, thus F is Incomplete by your definition above. Part of the key of the Godel proof is that while G sort of refers to itself, it does it in a way that F can't handle, so |

Posted: 22 Days 4 Hours ago by: Julio Di Egidio Or a programmer for that sake, that fucking moron just full of shit. But it's NOT OK to cross-spam 5 Usenet groups with just your personal demented chats. Eat shit and die you all. Julio |

Posted: 22 Days 9 Hours ago by: olcott It is OK that you are not a math guy. If you were a math guy you would understand that if G is provable then that makes Gödel totally wrong. G is not Gödel's theorem, it is a key element of his theorem. Incomplete T means that there |

Posted: 22 Days 10 Hours ago by: Ben G is provable. Proofs abound. I was pointing out one in a proper proof assistant, Coq. |

Posted: 22 Days 11 Hours ago by: olcott It is true that G is not provable. G is not provable because it is semantically incorrect in the exactly same way that the Liar Paradox is semantically incorrect. Gödel says: 14 Every epistemological antinomy can likewise be used for |

Posted: 22 Days 11 Hours ago by: Richard Damon Except that, I believe, in Prolog, all expression are considered to be either True or False (and default to being called false if they aren't given as True or provable by the system as True. Yes, there is a Unification test that allows |

Posted: 22 Days 11 Hours ago by: olcott So we still have not gotten to a best way to encode the Liar Paradox. |

Posted: 22 Days 11 Hours ago by: olcott Coq is not an automated theorem prover https://en.wikipedia.org/wiki/Coq In other words it is based on the sound deductive inference model. |

Posted: 22 Days 12 Hours ago by: Julio Di Egidio LOL, that rather tells about your reading abilities. Go fuck yourself, you utter imbecille, you and the whole indecent bandwagon. *Plonk* Julio |

Posted: 22 Days 12 Hours ago by: Julio Di Egidio That's just another piece of nonsense, GIT can be formalised in BASIC for that sake. You bunch of spamming absolute assholes and spammers of all poonds, indeed Olcott is your good measure. *Plonk* Julio |

Posted: 22 Days 12 Hours ago by: olcott I might take a look at it. The key advantage of Prolog that that by basing its analysis on facts and rules and having negation as failure it corrects all of the errors of formal logic systems. Prolog does not make the mistake of assumi |

Posted: 22 Days 12 Hours ago by: Ben And indeed there is a fully formalised proof of GIT in Coq (though I think it's the slightly tighter Gödel-Rosser version). |

Posted: 22 Days 12 Hours ago by: Aleksy Grabowski I've already wrote it in one of my previous posts, I just didn't want to repeat myself: I probably have found your profile on the internet and I conclude that your arrogance directly stems from your lack of any formal education. You |

Posted: 22 Days 13 Hours ago by: Julio Di Egidio Prolog is a Turing-complete language, duh. When Dunning-Kruger is a compliment... Get the fuck out of comp.lang.prolog. *Plonk* Julio |

Posted: 22 Days 13 Hours ago by: Aleksy Grabowski Thanks for confirmation, that's what exactly what I was trying to tell to topic poster in one of my previous posts. Prolog in it's bare form is a bad theorem solver. It wasn't designed a such. If you want to deal with such problems mayb |

Posted: 22 Days 13 Hours ago by: Richard Damon TRANSLATION: I trim out what will prove me wrong because I don't have time to think up other excuses. You are just admitting failure, if not to yourself, to anyone with a real brain. Nope, NOT extraneous, just apparently beyound your |

Posted: 22 Days 14 Hours ago by: Richard Damon IF you are defining that your logic system is limited to what Prolog can "Prove", that is fine. Just realize that you have just defined that your logic system can't handle a lot of the real problems in the world, and in particular, it |

Posted: 22 Days 14 Hours ago by: Aleksy Grabowski This still is incorrect. First of all, enable tracing: ?- trace. true. Then *execute* the predicates that you are trying to use: [trace] ?- LP = \+(LP), call(LP). Call: (11) _6566=(\+_6566) ? creep Exit |

Posted: 22 Days 14 Hours ago by: olcott That is why I updated it to this: ?- LP = \+(LP). LP = (\+LP). ?- unify_with_occurs_check(LP, \+(LP)). false. |

Posted: 22 Days 14 Hours ago by: Aleksy Grabowski Sadly you aren't using Prolog correctly. You still have to *execute* predicates, because right now they don't mean anything. You can try to enable predicate tracer and see for yourself that neither \+ nor `true` is ever executed. To e |

Posted: 22 Days 15 Hours ago by: olcott Here it is even simpler: ?- LP = \+(LP). LP = (\+LP). ?- unify_with_occurs_check(LP, \+(LP)). false. |

Posted: 22 Days 15 Hours ago by: olcott I do see that it is rejected by SWI Prolog: ?- assertz( (g :- \+ g) ). true. ?- g. ERROR: Out of local stack ?- This one seems to work: ?- LP = \+(true(LP)). LP = (\+true(LP)). ?- unify_with_occurs_check(LP, \+(true(LP))). false. |

Posted: 22 Days 15 Hours ago by: Aleksy Grabowski You have said it incorrectly. Prolog program has two different parts: knowledge base and a query. Knowledge base is usually loaded from the text file before starting Prolog runtime. Query can be asked using interactive prompt. The ge |

Posted: 22 Days 16 Hours ago by: olcott (SWI-Prolog (threaded, 64 bits, version 7.6.4) Predicate not/1 not(:Goal) True if Goal cannot be proven. Retained for compatibility only. New code should use \+/1. https://www.swi-prolog.org/pldoc/man?predicate=not/1 SWI Prolog does n |

Posted: 22 Days 16 Hours ago by: Aleksy Grabowski In this expression, `not` is treated as a term — a symbol without any meaning, just text "not", and not the _negation_. If you want to check if a variable can be different from itself you can try this: ?- dif(X, X). But, remem |

Posted: 22 Days 16 Hours ago by: olcott My key more important understanding of the fundamental architecture of Prolog is that it is anchored in sound deductive inference thus correctly all of the errors that have crept into logic since Aristotle's syllogism. Start with know |

Posted: 22 Days 17 Hours ago by: olcott Yes Jeff is mostly a Jackass. Once in a very great while he says something interesting. This is very rare yet thankfully more often than never. |

Posted: 22 Days 17 Hours ago by: olcott I would say that you did an excellent job of that. What do you think of this version: ?- LP = not(LP). LP = not(LP). ?- unify_with_occurs_check(LP, not(LP)). false. The "not" of Prolog's "negation as failure" already means not(true(LP) |

Posted: 22 Days 17 Hours ago by: olcott Encoding "This sentence is not true" in Prolog: ?- LP = not(LP). LP = not(LP). ?- unify_with_occurs_check(LP, not(LP)). false. The "not" of Prolog's "negation as failure" already means not(true(LP)) when we assume that true(LP) means |

Posted: 22 Days 17 Hours ago by: olcott ?- LP = not(LP). LP = not(LP). ?- unify_with_occurs_check(LP, not(LP)). false. I simplified it because the "not" of Prolog "negation as failure" already means not(true(LP)) when we assume that true(LP) means provable(LP). This versio |

Posted: 22 Days 17 Hours ago by: Mr Flibble The ad hominem attack is a logical fallacy: so it is in fact YOU who is throwing excrement at the walls, not Olcott. Attack the argument not the person, dear. https://en.wikipedia.org/wiki/Ad_hominem /Flibble |

Posted: 22 Days 18 Hours ago by: Julio Di Egidio No, you didn't, and I have said why twice by now. You bring it up: and it is in fact irrelevant here, as long as the original question is the question you noticed it is. Anyway, discussing with Olcott's interlocutors is always even wor |

Posted: 22 Days 18 Hours ago by: Aleksy Grabowski The request from topic poster was — how would I represent sentence "This sentence is not provable". I came up with some small example of "not provable sentence" which happens to be a simple infinite loop. I did *not* claim that it ca |

Posted: 22 Days 19 Hours ago by: Jeff Barnett On 5/2/2022 9:24 AM, olcott wrote: NOTHING OF VALUE I will attempt to summarize the level of the idiot's understanding of Prolog: The level is the same as of his understanding of math, logic, C, C++, software engineering, programming, p |

Posted: 22 Days 19 Hours ago by: Julio Di Egidio And as I have pointed out to you, your "solution" solves nothing at all. That's just nonsense: Prolog is a formal language no less than any other. Plus you too must think you have a solution to the halting problem... Enough said. Juli |

Posted: 22 Days 19 Hours ago by: olcott I need to know more details about what is occurring internally (within Prolog) when the expressions are executed. The above quote from Clocksin & Mellish refers to getting unify_with_occurs_check to check in advance that unification w |

Posted: 22 Days 19 Hours ago by: Aleksy Grabowski As I have said previously, my example is naïve. Maybe if you will think hard enough you can make it detect such conditions, probably by writing meta-interpreter of some sort, and terminate. Personally, I don't think that using Prolog |

Posted: 22 Days 20 Hours ago by: olcott What is occurring internally with Prolog's evaluation of the above expressions? Does it build an infinite structure? I think that I have refuted the conventional proofs of the halting problem. I spent a man-year creating the x86 operat |

Posted: 22 Days 20 Hours ago by: olcott That is beautiful and affirms the key element of all of my research on incompleteness. This is the mathematical definition of incompleteness: Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)). It says expression φ of formal system |

Posted: 22 Days 20 Hours ago by: Julio Di Egidio g:-\+g as g:-g are literally and simply infinite loops: neither captures anything deep about anything. Aka plain and simple divergent computation. Yes, but even if it didn't, it'd be you at some point who would have to switch it off. |

Posted: 22 Days 20 Hours ago by: olcott That is exactly what I expected. Does it crash because it ran out of memory? unify_with_occurs_check is supposed to determine in advance that unification will crash. Can it be applied to the above? Do we have any Prolog that shows in a |

Posted: 22 Days 20 Hours ago by: Aleksy Grabowski Some definitions. The part before `:-` is called head, and after is called body. Conceptually the model of execution of Prolog programs looks more-or-less as follows: 0. If predicate doesn't have body it is always true. 1. Assume t |

Posted: 22 Days 21 Hours ago by: olcott That is great. That shows when Gödel's 1931 Incompleteness Theorem is transformed into its barest possible essence Prolog proves it to be ill-formed. What is happening internally that causes the expression to never terminate? |

Posted: 22 Days 21 Hours ago by: Aleksy Grabowski Yep, that's exactly what I was saying. IMHO, the only correct behavior is to go to infinite loop and refuse to give any answer. |

Posted: 22 Days 21 Hours ago by: Julio Di Egidio As long as it's equal to "<whatever> is not provable", that's just any proposition <whatever> that fails, e.g. g :- fail. As to how to rather encode self-referentiality, and to begin with one needs first-order, that's something to think |

Posted: 22 Days 21 Hours ago by: Mostowski Collapse The SWI-Prolog built-in with_output_to/2 does also not work. Would need something like a with_error_to/2 ? Does this exist? I only get: ?- with_output_to(atom(_), (write('I am chatty'), nl)). true. ?- with_output_to(atom(_), string_ter |

Posted: 22 Days 21 Hours ago by: Mostowski Collapse I didn’t start a new testing campaign with pPEG yet, where I get a new type of error, which I do not yet know how to silence. But meanwhile I have a funny test case where SWI-Prolog and SICStus disagree: /* SWI-Prolog */ ?- X = (- - |

Posted: 22 Days 22 Hours ago by: Aleksy Grabowski "This sentence is provable" g. Both of sentences are true at the same time: both :- g, \+ g. Then query: ?- both. doesn't terminate, which is correct behavior for such paradoxical statement. Did you expect some answe |

Posted: 22 Days 22 Hours ago by: olcott That is great, now what happens when we encode: "This sentence is provable" in Prolog? What happens when we test both of these with unify_with_occurs_check ? None-the-less by evaluating expressions on the basis of facts (expression k |

Posted: 22 Days 22 Hours ago by: Aleksy Grabowski g :- \+ g. Then you can ask Prolog if this sentence is true: ?- g. Prolog will give you the only correct answer — no answer 🙃. Prolog by itself is a very bad theorem prover and it is very limited framework for formal logic, beca |

Posted: 22 Days 23 Hours ago by: olcott I trim so that we can stay focused on the point at hand and not diverge into many unrelated points. The main way that all of the rebuttals of my work are formed is changing the subject to another different subject and the rebutting thi |

Posted: 22 Days 23 Hours ago by: olcott Here is what I understand of the relationship between logic and Prolog. Prolog corrects all of the errors of classical and symbolic logic by forming the underlying framework for the correct notion of truth and provability. In all of the |

Posted: 23 Days ago by: Aleksy Grabowski Wow, I went offline for a weekend, because we had such a nice weather, and this thread exploded to enormous size 😲. I didn't read the whole thread it's just too big. On 5/1/22 13:00, olcott wrote: I don't want to undermine your know |

Posted: 23 Days 1 Hour ago by: Richard Damon I will acknowledge that you have proven yourself to be the lying bastard. YOU have REPEADTEDLY trimmed out important parts of the conversation either to INTENTIONALLY be deceptive, or because you are so incompetent at this material tha |

Posted: 23 Days 7 Hours ago by: Markus Triska Frequently Asked Questions - comp.lang.prolog Last-modified: 2022-02-24 Last-changes: Update link to tutorial by J.R. Fisher. Geoffrey Churchill. Markus Triska (Mar. 2 2007 - ... ) Remko Troncon (Jan. 6 2002 - Mar |

Posted: 23 Days 8 Hours ago by: André G. Isaak There is no quote where Gödel claims G is "sufficiently equivalent" to the Liars Paradox. (And "sufficiently equivalent" for what, exactly? Is a five dollar bill "sufficiently equivalent" to 20 quarters? It's a meaningless question w |

Posted: 23 Days 9 Hours ago by: olcott He is focusing on the dishonest dodge of the strawman error by making sure to ignore that in another quote Gödel said that Gödel's G is sufficiently equivalent to the Liar Paradox on the basis that the Liar Paradox is an epistemologi |

Posted: 23 Days 9 Hours ago by: Richard Damon You mean like when he said (and you snipped): Maybe you should check your OWN facts. He is CLEARLY not saying that the Liar Paradox can't be used for this sort of proof, because he talks about its form being used. What he is denying, |

Posted: 23 Days 9 Hours ago by: André G. Isaak I didn't so much deny that as I did claim it was vacuous and irrelevant. Gödel draws a parallel between his proof and The Liar. He also notes that other antinomies could be used to construct similar proofs. That would seem to mean t |

Posted: 23 Days 10 Hours ago by: olcott If you look at the actual facts you will see that he continued to deny that kept continuing to deny that the Liar Paradox can be used for similar undecidability proofs at least a half dozen times. If you make sure to knowingly contradi |

Posted: 23 Days 10 Hours ago by: Richard Damon No, he says that the use of the Liar Paradox in the form that Godel does doesn't make the Godel Sentence a non-truth holder. The fact that you have mis-interpreted him that many times, and even snipped out his explanations shows you ig |

Posted: 23 Days 10 Hours ago by: olcott If you look at the full context of many messages you will see that he kept continuing to deny that the Liar Paradox can be used for similar undecidability proofs at least a half dozen times. Only when I made denying this look utterly r |

Posted: 23 Days 10 Hours ago by: Richard Damon So, No. Note a trimming to change meaning, the original was: So, clearly the requested proof was that about USING the epistemolgocal antinomy and it being just like one so not a Truth Bearer. Note, the comment that you claimed you bac |

Posted: 23 Days 11 Hours ago by: olcott I backed André into a corner and forced him to quit lying On 5/1/2022 6:44 PM, André G. Isaak wrote: |

Posted: 23 Days 11 Hours ago by: olcott I backed him into a corner and forced him to stop lying: On 5/1/2022 6:44 PM, André G. Isaak wrote: Anyone that abuses me gets a metaphorical uppercut to the jaw. |

Posted: 23 Days 12 Hours ago by: olcott See that I backed you into a corner to force you to quit lying. |

Posted: 23 Days 12 Hours ago by: André G. Isaak Equivalence with respect to *what*? If two things are equivalent but not identical, it means they are equivalent with respect to some things but not equivalent with respect to others. The entire point of my posts has been to clarify s |

Posted: 23 Days 12 Hours ago by: olcott Not quite. X = is an epistemological antinomy Of course not nitwit, you know that I mean equivalence. What kind of stupid fool would believe that I mean that G and LP are one and the same thing? I know, I know, a jackass that wants to |

Posted: 23 Days 13 Hours ago by: André G. Isaak Presumably he will point to the (nonexistent) footnote where Gödel claims that The Liar and G are "sufficiently equivalent" rather than the (actual) footnote where Gödel rather explicitly denies this. André |

Posted: 23 Days 13 Hours ago by: Richard Damon As Andre pointed out, when you look at the statement to see what the terms are, you just agreed with him and proved that YOU are the Liar. |

Posted: 23 Days 13 Hours ago by: Richard Damon You can PROVE it? Note, that means you need to start with the ACTUAL G that Godel used, not some "simplified" version. So you better know what all that means. |

Posted: 23 Days 13 Hours ago by: olcott I just proved that you are a lying bastard. I can very easily forgive and forget, what I will not do is tolerate mistreatment 14 Every epistemological antinomy can likewise be used for a similar undecidability proof The Liar Paradox i |

Posted: 23 Days 13 Hours ago by: André G. Isaak For christ's sake. You can't even see the irrelevance of the above. Let's consider what the X and Y are in the above: X would be 'Is an Antinomy' Since Gödel was *already* talking about The Liar, Y is "Can be used to form an undecida |

Posted: 23 Days 13 Hours ago by: olcott I just proved that you are a lying bastard. I can very easily forgive and forget, what I will not do is tolerate mistreatment 14 Every epistemological antinomy can likewise be used for a similar undecidability proof The Liar Paradox i |

Posted: 23 Days 13 Hours ago by: olcott sufficiently equivalent |

Posted: 23 Days 13 Hours ago by: André G. Isaak Since you're clearly not planning on addressing any of my points, I think we're done. I'll leave you with a small multiple choice quiz: Are you (a) someone who was dropped on their head as a child. (b) suffering from foetal alcohol sy |

Posted: 23 Days 14 Hours ago by: Richard Damon So, there is a difference between being used for and being just like. |

Posted: 23 Days 14 Hours ago by: olcott 14 Every epistemological antinomy can likewise be used for a similar undecidability proof and the Liar Paradox is and is an epistemological antinomy you lying bastard. |

Posted: 23 Days 14 Hours ago by: olcott 14 Every epistemological antinomy can likewise be used for a similar undecidability proof and the Liar Paradox is and is an epistemological antinomy you lying bastard. |

Posted: 23 Days 15 Hours ago by: Richard Damon Right, But G isn't, because it ISN'T the Liar's Paradox, but has a structure based on the Liar's Paradox but transformed. Your failure to understand this difference says you are unqualified to talk about the meaning of words, or basic |

Posted: 23 Days 15 Hours ago by: André G. Isaak The only one being dishonest here is you as you keep snipping the substance of my post. Gödel claims there is a *close relationship* between The Liar and G. He most certainly does *not* claim that they are the same. (That one can con |

Posted: 23 Days 15 Hours ago by: olcott You freaking dishonest bastard 14 Every epistemological antinomy can likewise be used for a similar undecidability proof The Liar Paradox is an epistemological antinomy |

Posted: 23 Days 16 Hours ago by: Richard Damon So something based on another thing is that other thing? Does that mean your automobile is just a pile of gasoline? That IS the argument you are making boiled down to simple terms. |

Posted: 23 Days 16 Hours ago by: olcott 14 Every epistemological antinomy can likewise be used for a similar undecidability proof Therfore the liar paradox can likewise be used for a similar undecidability proof, nitwit. I would not call you a nitwit except that you so persist |

Posted: 23 Days 16 Hours ago by: André G. Isaak And what does any of the above have to do with what I state below? That's your faulty attempt at expressing The Liar in Prolog, which has nothing to do with Gödel's G. G has *a relationship* to The Liar, but G is *very* different from |

Posted: 23 Days 16 Hours ago by: olcott Do I have to say the same thing 500 times before you bother to notice that I said it once? 14 Every epistemological antinomy can likewise be used for a similar undecidability proof Therefore LP ↔ ~True(LP) can be used for a similar |

Posted: 23 Days 17 Hours ago by: Richard Damon Well, for Godel's G, since it is just that a statement that some statement x is provable, and the provability of a statement is ALWAYS a Truth Bearer, as you can't prove a non-sense sentence, so provable(x) would be false is x is not a |

Posted: 23 Days 17 Hours ago by: olcott My original thinking was that (1) and (2) and the Liar Paradox all demonstrate the exact same error. I only have considered (3) in recent years, prior to that I never heard of (3). The category error would be that none of them is in th |

Posted: 23 Days 18 Hours ago by: olcott I do think that your idea of "category error" is a brilliant new insight into pathological self-reference problems such as: (1) The Halting Problem proofs (2) Gödel's 1930 Incompleteness (3) The 1936 Undefinability theorem It very succ |

Posted: 23 Days 18 Hours ago by: Richard Damon Maybe it just says that PROLOG can't express the statement without an infinite cycle due to the limitiations in Prologs logic system? Better logic systems can handle and work with statements that are self-referential or recursive. You |

Posted: 23 Days 18 Hours ago by: Richard Damon Incorrect, conventional logic understand that some statements are not truth bearers. Now, a lot of rules are pre-conditioned on the assumption that their inputs ARE truth bearers, so you need to be careful in just applying rules to sta |

Posted: 23 Days 19 Hours ago by: Richard Damon You think? depends on what you know about the definition of foo. Perhaps you can't do anything with the infinitely expanded version, since you can't actually express it, but the self-referential version might be able to be analyzed. Y |

Posted: 23 Days 19 Hours ago by: Jeff Barnett T24gNS8xLzIwMjIgNjoxOSBBTSwgTXIgRmxpYmJsZSB3cm90ZToNCj4gT24gU2F0LCAzMCBB cHIgMjAyMiAyMzoyNDowNSAtMDYwMA0KPiBKZWZmIEJhcm5ldHQgPGpiYkBub3RhdHQuY29t PiB3cm90ZToNCj4gDQo+PiBPbiA0LzMwLzIwMjIgOToxNSBQTSwgb2xjb3R0IHdyb3RlOg0K Pj4+IE9uIDQvMzAvMjAyM |

Posted: 23 Days 19 Hours ago by: André G. Isaak Yes. There is a close *relationship* between his G and The Liar. That does *not* mean that G *is* The Liar. It is not. But you refuse to read Gödel's actual math to see the *very* significant differences between the two. Similarly o |

Posted: 23 Days 19 Hours ago by: Richard Damon But if you don't know N, you don't know when to terminate the expansion. If all you know is that N is a positive integer, then you don't know when to stop. That is the issue, Fact of N isn't just defined for know values of N, but you |

Posted: 23 Days 19 Hours ago by: Richard Damon No, not "incorrect", just "can't be handled by Prolog". If foo is my fact() function, it is definitely "defined". |

Posted: 23 Days 19 Hours ago by: Richard Damon Depends on the definition of foo. If foo is the function "fact" I have presented, then the unwinding becomes exactly that to a too dumb naive expansion. Thus "never" is incorrect. Because Prolog is too limited to be able to fully h |

Posted: 23 Days 19 Hours ago by: olcott It says that Every epistemological antinomy can likewise be used for a similar undecidability proof thus even English epistemological antinomies such as the Liar antinomy can be used. Gödel says: "There is also a close relationship w |

Posted: 23 Days 20 Hours ago by: olcott That it not what Gödel says: 14 Every epistemological antinomy can likewise be used for a similar undecidability proof G ↔ ¬Provable(F, G) is an epistemological antinomy therefore it is necessarily sufficient. Likewise with this |

Posted: 23 Days 20 Hours ago by: polcott This type is never fine: // Adapted from Clocksin & Mellish foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))) Because Gödel says 14 Every epistemological antinomy can likewise be used for a similar undecidability proof G |

Posted: 23 Days 23 Hours ago by: polcott Brilliantly well put. |

Posted: 24 Days ago by: Mr Flibble Are you mental? That definition isn't infinitely recursive as it terminates when N equals 1 given a set of constraints on N (positive integer greater or equal to 1). /Flibble |

Posted: 24 Days ago by: olcott The expression inherently has an infinite cycle, making it erroneous. Does not have an infinite cycle. It always begins with a finite integer that specifies the finite number of cycles. An infinite cycle is the same thing as an infin |

Posted: 24 Days ago by: Richard Damon So, factorials don't nave valid logical meaning? That is the logical conclusion of your statement since fact does the same expansion. Shows the capability of your logic system. "encoded in Prolog", nope, becuase G uses logic that is b |

Posted: 24 Days ago by: olcott Semantically incorrect expressions of language are totally invisible to conventional logic because conventional logic incorrectly assumes that every expression is true or false. Prolog can detect expressions that are neither true nor f |

Posted: 24 Days ago by: Richard Damon You misunderstand what it says. It says that it can't figure how to express the statement without a cycle. That is different then taking infinite memory. It only possibly implies infinite memory in a naive expansion, which isn't the on |

Posted: 24 Days ago by: olcott It correctly says that this is what the expression means: foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))) Which means that it does not have a valid logical meaning. This says that G is logically equivalent to its own unp |

Posted: 24 Days ago by: Richard Damon "Better" is as subjective word unless you define an objective criteria. The fact that Prolog doesn't have the expresiability to actually write the Godel sentence, means it can't actually be used to disprove it. Misusing notations to sh |

Posted: 24 Days ago by: Richard Damon Which just shows PROLOG can't handle that sort of expression, not that it logically doens't have a meaning. So all Clocksin & Melish is saying is that such an expression fails in PROLOG, not that it doesn't have a valid logical meanin |

Posted: 24 Days ago by: olcott That is counter-factual. unify_with_occurs_check determines that it would require infinite memory and then aborts its evaluation. foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))) "..." indicates infinite depth, thus infin |

Posted: 24 Days ago by: olcott That is the dishonest dodge of the strawman error. The particular expression at hand is inherently incorrect and thus any system that proves it is a broken system. foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(foo(...)))))))))))) The ". |

Posted: 24 Days ago by: olcott Prolog has a better model in that it can detect semantic paradoxes. LP ↔ ¬True(LP) is correctly assessed as neither true nor false. |

Posted: 24 Days ago by: olcott The question is not whether some infinite structures have meaning that is the dishonest dodge of the strawman error. The question is whether on not the expression at hand has meaning or is simply semantically incoherent. I just posted |

Posted: 24 Days 1 Hour ago by: olcott *You can and Prolog can detect and reject it* BEGIN:(Clocksin & Mellish 2003:254) Finally, a note about how Prolog matching sometimes differs from the unification used in Resolution. Most Prolog systems will allow you to satisfy goals |

Posted: 24 Days 1 Hour ago by: Richard Damon Nope, a tree that one branch points into itself higher up represents a tree with infinite depth, but only needs a finite amount of memory. Building such a structure may require the ability to forward declare something or reference some |

Posted: 24 Days 1 Hour ago by: Richard Damon As Jeff pointed out, your claim is shown false, that some statements with infinite expansions can be worked with by some automatic solvers. This just proves that you don't really understand the effects of "recursion" and "self-referenc |

Posted: 24 Days 1 Hour ago by: Richard Damon So you are sort of answering your own question. The model of logic that Prolog handles isn't quite the same as "conventional" logic, in part due to the way it (doesn't) define Logical Negation. This seems to fit into your standard misu |

Posted: 24 Days 1 Hour ago by: olcott That is incorrect. any structure that is infinitely deep would take all of the memory that is available yet specifies an infinite amount of memory. This says that G is logically equivalent to its own unprovability in F G ↔ ¬(F ⊢ G |

Posted: 24 Days 1 Hour ago by: olcott Is says that it is. It says that "not" is synonymous with \+. |

Posted: 24 Days 1 Hour ago by: olcott negation, not, \+ The concept of logical negation in Prolog is problematical, in the sense that the only method that Prolog can use to tell if a proposition is false is to try to prove it (from the facts and rules that it has been told |

Posted: 24 Days 2 Hours ago by: Mikko Doesn't matter as you can't give an infinite expression to a theorem prover. Mikko |

Posted: 24 Days 2 Hours ago by: Mikko Another Prolog implementation might interprete LP = not(true(LP)) differently and still conform to the prolog standard. When discussing data structures, "infinite" and "loop" mean the same. The data structure is infinitely deep but con |

Posted: 24 Days 3 Hours ago by: Mikko Note that the negation discussed above is not present in LP = not(true(LP)). Mikko |

Posted: 24 Days 3 Hours ago by: Mikko That's correct. Prolog language does not give any inherent semantics to data structures. It only defines the execution semantics of language structures and standard library symbols. Those same synbols can be used in data structures with |

Posted: 24 Days 7 Hours ago by: Jeff Barnett T24gNC8zMC8yMDIyIDk6MTUgUE0sIG9sY290dCB3cm90ZToNCj4gT24gNC8zMC8yMDIyIDEw OjExIFBNLCBSaWNoYXJkIERhbW9uIHdyb3RlOg0KPj4gT24gNC8zMC8yMiAxMDo1NiBQTSwg b2xjb3R0IHdyb3RlOg0KPj4+IE9uIDQvMzAvMjAyMiA5OjM4IFBNLCBSaWNoYXJkIERhbW9u IHdyb3RlOg0KPj4+PiBPb |

Posted: 24 Days 7 Hours ago by: olcott What about this one? LP ↔ ¬True(LP) // Tarski uses something like this https://liarparadox.org/Tarski_275_276.pdf or this one? G ↔ ¬(F ⊢ G) |

Posted: 24 Days 9 Hours ago by: olcott Not in this case, it is very obvious that no theorem prover can possibly prove any infinite expression. It is the same thing as a program that is stuck in an infinite loop. |

Posted: 24 Days 9 Hours ago by: Richard Damon And it appears that you don't understand it, because you still make category errors when trying to talk about it. Right. but some infinite structures might actually have meaning. The fact that Prolog uses certain limited method to fig |

Posted: 24 Days 9 Hours ago by: olcott In this case it does. I have spent thousands of hours on the semantic error of infinitely recursive definition and written a dozen papers on it. Glancing at one of two of the words of Clocksin & Mellish does not count as reading it. BE |

Posted: 24 Days 9 Hours ago by: Richard Damon I did. You just don't seem to understand what I am saying because it is above your head. Prolog is NOT the defining authority for what is a valid logical statement, but a system of programming to handle a subset of those statements (a |

Posted: 24 Days 10 Hours ago by: olcott It is really dumb that you continue to take wild guesses again the verified facts. Please read the Clocksin & Mellish (on page 3 of my paper) text and eliminate your ignorance. |

Posted: 24 Days 10 Hours ago by: Richard Damon No, that IS what they say, that this sort of recursion fails the test of Unification, not that it is has no possible logical meaning. Prolog represents a somewhat basic form of logic, useful for many cases, but not encompassing all pos |

Posted: 24 Days 10 Hours ago by: olcott I asked the question incorrectly, what I really needed to know is whether or not the Prolog correctly encodes this logic sentence: LP := ~True(LP) x := y means x is defined to be another name for y https://en.wikipedia.org/wiki/List_of_ |

Posted: 24 Days 10 Hours ago by: olcott That is not what Clocksin & Mellish says. They say it is an erroneous "infinite term" meaning that it specifies infinitely nested definition like this: LP := ~True(LP) specifies: ~True(~True(~True(L~True(L~True(...)) The ellipses "..." |

Posted: 24 Days 11 Hours ago by: Richard Damon Since it isn't giving you a "syntax error", it is probably correct Prolog. Not sure if your interpretation of the results is correct. All that false means is that the statement LP = not(true(LP)) is recursive and that Prolog can't ac |

Posted: 24 Days 15 Hours ago by: olcott negation, not, \+ The concept of logical negation in Prolog is problematical, in the sense that the only method that Prolog can use to tell if a proposition is false is to try to prove it (from the facts and rules that it has been told |

Posted: 24 Days 15 Hours ago by: olcott The above is the actual execution of actual Prolog code using (SWI-Prolog (threaded, 64 bits, version 7.6.4). According to Clocksin & Mellish it is not a mere loop, it is an "infinite term" thus infinitely recursive definition. I am tr |

Posted: 24 Days 18 Hours ago by: Aleksy Grabowski I just want to add some small note. This "not(true(_))" thing is misleading. Please note that it is *not* a negation. Functionally it is equivalent to: X = foo(bar(X)). On 4/30/22 11:31, Mikko wrote: |

Posted: 24 Days 20 Hours ago by: Mostowski Collapse Charles Lutwidge Dodgson https://de.m.wikipedia.org/wiki/Lewis_Carroll Do I have permission from https://math.stackexchange.com/users/742/arturo-magidin To cite wikipedia? Mostowski Collapse schrieb am Samstag, 30. April 2022 um 17:38 |

Posted: 24 Days 20 Hours ago by: Mostowski Collapse Maybe the war between French and British is nevertheless over, the Lady showed in one scene a logic booklet by Lewis Caroll. Or maybe the lady though Caroll is a french name? Dont know where this name is from. Could be Czech? P.S.: Cou |

Posted: 25 Days ago by: Mostowski Collapse Concerning parenthesis I only found this bug, but its not really parenthesis related. So unlike Trealla it could be that parenthesis are not a problem. This here gives the same associativity hickup with and without parenthesis: ?- string |

Posted: 25 Days ago by: Mostowski Collapse This is an interesting pPEG example bug. Actually I wanted to hunt parenthesis parsing bugs, so I was up to generating some test cases that contain parenthesis. But this test case doesn’t contain any parenthesis, but it seems a binary in |

Posted: 25 Days 3 Hours ago by: Mikko This is correct but to fail would also be correct. unify_with_occurs_check must fail if the unified data structure would contain loops. Mikko |

Posted: 25 Days 5 Hours ago by: olcott ?- LP = not(true(LP)). LP = not(true(LP)). ?- unify_with_occurs_check(LP, not(true(LP))). false. (SWI-Prolog (threaded, 64 bits, version 7.6.4) https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_ |

Posted: 25 Days 20 Hours ago by: Mostowski Collapse But this is a much too benevolent interpretation, possibly José Carlos Santos is just a pervert, that saw somebody with 101 points and started a fight. LoL Mostowski Collapse schrieb am Freitag, 29. April 2022 um 18:25:31 UTC+2: |

Posted: 25 Days 20 Hours ago by: Mostowski Collapse Social science researchers call this the SIQQ effect, social IQ degradation effect. So when mathematics act as a pack of wolf, they all eject their brains. A little bit related to the Zollman Effect: Our conjecture is that the cycle will |

Posted: 26 Days ago by: Mostowski Collapse If you take into account the Peano apostroph, its definitively more than 100 years old stuff. Peano used the apostroph (1888?) in geometry to denote a shadow. But guess what: dom(f): The shadow of f on the x-axis img(f): The shadow of f |

Posted: 26 Days ago by: Mostowski Collapse But I guess that trolling me has to do, that my answers was the only serious answers, and the remaining answers, I deleted my two answers, are troll answers, which will leave Dan Christensen totally in the dark. One answer circumewents i |

Posted: 26 Days ago by: Mostowski Collapse Shoenfield publish in 1960 bit I guess from 1950. So around 70 years. But I am waiting for the moment that a ruSSian Nazi comes around the corner and declares set theory Nazi. Altreay the stack exchange Nazis cannot digest that the real |

Posted: 26 Days ago by: Mostowski Collapse Blame it on Robert Kowalski, he even creates an artificial Schism between Edinburgh Prolog and Colmerauer Prolog in the video, But guess what the name "Kowalski" is not British, thats rather something Polish. There really exists somethin |

Posted: 26 Days 1 Hour ago by: Mostowski Collapse Why is there no coverage of the ISO core standard, maybe I didn't watch it closely... ? Do the French hate the British so much, that they would like to beton the Channel Tunnel? LoL P.S.: I slowly start hating the Portuguese because of |

Posted: 26 Days 1 Hour ago by: Mostowski Collapse I implemented this already for the full fledged parser. But the simplified version doesn’t have it yet, because the simplified version didn’t parse a list of period terminated terms anyway yet. If I have time I will do the simplified |

Posted: 26 Days 1 Hour ago by: Mostowski Collapse I am little bit behind schedule of a Fuzzer that also does parenthesis. So this was my sixth sense. Was also working on another front, resyncing after errors. I found a solution today: Have a grammer that covers non-errorneous sentences a |

Posted: 26 Days 1 Hour ago by: Mostowski Collapse More proof that Logtalk is utter nonsense. What does the Logtalk test suite even test concerning the various "adapters" it has, like Trealla? This is a nice gem: $ ./tpl -v Trealla Prolog (c) Infradig 2020-2022, v1.27.12-31-g3575df $ ./t |

Posted: 26 Days 3 Hours ago by: Mostowski Collapse Its amazing that 100 years set theory, this goblet has surely passed this person, not only Dan Christensen. Mostowski Collapse schrieb am Freitag, 29. April 2022 um 11:09:47 UTC+2: |

Posted: 26 Days 3 Hours ago by: Mostowski Collapse No wonder Logtalk is such a nonsense. This dickhead from Porto has no clue about mathematics. He even doesn't understand this fallacy: /* Not Provable */ f e B^A => rng(f) = B José Carlos de Sousa Oliveira Santos https://www.fc.up.pt/ |

Posted: 26 Days 22 Hours ago by: Paulo Moura Hi, Logtalk 3.55.0 is now available for downloading at: https://logtalk.org/ This release adds Windows PowerShell versions of the setup, integration, embedding, and tools Bash shell scripts (joint work with Hans N. Beck); includes new a |

Posted: 28 Days 1 Hour ago by: Mostowski Collapse Can your Prolog system run this example indefinitely? ?- A=(1=1,call(A)), A. But there is much more than what meets the eye. Dogelog Player is a 100% Prolog written Prolog interpreter that runs on the Python and JavaScript platform. It |

**245** recent articles found.

clearneti2ptor