3 ms·

This is very neat. It shows that Prolog is very close to being the holy grail of an executable specification language. But my question was about verification: T

This is very neat. It shows that Prolog is very close to being the holy grail of an executable specification language. But my question was about verification: TLA+ is not just used for modeling but also for proving stuff about the models. Do you have anything similar for Prolog? If yes, I would love to use it :-) If you're only interested in the specification part of TLA+ but in proofs, that's great. But then it's not fair to claim that you can do everything in Prolog that TLA+ does.

carapace 7y ago
> This is very neat. Cheers! > Do you have anything similar for Prolog? Well, what you think of "Formal Methods: A First Introduction using Prolog to specify Programming Language Semantics"? https://homepage.cs.uri.edu/faculty/hamel/pubs/fcs16.pdf https://homepage.cs.uri.edu/faculty/hamel/pubs/fcs16.pdf Abstract > An important fundamental idea in formal methods is that programs are mathematical objects one can reason about. Here we introduce students and developers to these ideas in the context of formal programming language semantics. We use first-order Horn clause logic as implemented by Prolog both as a specification and a proof scripting language. A module we have written facilitates using Prolog as a proof assistant and insures that Prolog implements a sound logic. In order to illustrate our approach we specify the semantics of a small functional language and demonstrate various proof approaches and styles. I just found this the other day and it seems promising. > it's not fair to claim that you can do everything in Prolog that TLA+ does. A claim I didn't make. "So far", I said, and, "I'm not to far into it yet" (sic). :-) (Although it's trivially true because of Turing completeness, eh?) I have great respect for Lamport. I would hate to be unfair to him.
- tom_mellior 7y ago
  Oh, that paper is very interesting, thanks for that. It's not really comparable to a fully formal system, though: The user essentially chooses which trivial things to prove to convince themselves of something. For example, a real proof assistant would tell you what exactly to prove for the inductive proof in the factorial example. In this system you pick an induction principle yourself and hope it's correct. Still, I'd like to see more work along these lines.
  - carapace 7y ago
    It's Prolog, so there is probably already more. I just found a bachelor thesis from 2011 "Implementation of a Proof Assistant in Prolog" https://www2.imm.dtu.dk/pubdb/views/edoc_download.php/6043/pdf/imm6043.pdf https://www2.imm.dtu.dk/pubdb/views/edoc_download.php/6043/p... I haven't read it yet. There's also PRESS, which seems relevant, "Solving symbolic equations with PRESS" > We describe a program, PRESS, (PRolog Equation Solving System) for solving symbolic, transcendental, non-differential equations in one or more variables. PRESS solves autonomously, i.e. without guidance from the user. The methods used for solving equations are described, together with the service facilities. The principal technique, meta-level inference, appears to be relevant to the broader field of symbolic and algebraic manipulation. https://www.sciencedirect.com/science/article/pii/S0747717189800070 https://www.sciencedirect.com/science/article/pii/S074771718... https://github.com/maths/press https://github.com/maths/press I'm not trying to promote Prolog over TLA+ or anything, I've only just started with TLA+.

carapace 7y ago

> This is very neat. Cheers! > Do you have anything similar for Prolog? Well, what you think of "Formal Methods: A First Introduction using Prolog to specify Programming Language Semantics"? https://homepage.cs.uri.edu/faculty/hamel/pubs/fcs16.pdf https://homepage.cs.uri.edu/faculty/hamel/pubs/fcs16.pdf Abstract > An important fundamental idea in formal methods is that programs are mathematical objects one can reason about. Here we introduce students and developers to these ideas in the context of formal programming language semantics. We use first-order Horn clause logic as implemented by Prolog both as a specification and a proof scripting language. A module we have written facilitates using Prolog as a proof assistant and insures that Prolog implements a sound logic. In order to illustrate our approach we specify the semantics of a small functional language and demonstrate various proof approaches and styles. I just found this the other day and it seems promising. > it's not fair to claim that you can do everything in Prolog that TLA+ does. A claim I didn't make. "So far", I said, and, "I'm not to far into it yet" (sic). :-) (Although it's trivially true because of Turing completeness, eh?) I have great respect for Lamport. I would hate to be unfair to him.

tom_mellior 7y ago
Oh, that paper is very interesting, thanks for that. It's not really comparable to a fully formal system, though: The user essentially chooses which trivial things to prove to convince themselves of something. For example, a real proof assistant would tell you what exactly to prove for the inductive proof in the factorial example. In this system you pick an induction principle yourself and hope it's correct. Still, I'd like to see more work along these lines.
- carapace 7y ago
  It's Prolog, so there is probably already more. I just found a bachelor thesis from 2011 "Implementation of a Proof Assistant in Prolog" https://www2.imm.dtu.dk/pubdb/views/edoc_download.php/6043/pdf/imm6043.pdf https://www2.imm.dtu.dk/pubdb/views/edoc_download.php/6043/p... I haven't read it yet. There's also PRESS, which seems relevant, "Solving symbolic equations with PRESS" > We describe a program, PRESS, (PRolog Equation Solving System) for solving symbolic, transcendental, non-differential equations in one or more variables. PRESS solves autonomously, i.e. without guidance from the user. The methods used for solving equations are described, together with the service facilities. The principal technique, meta-level inference, appears to be relevant to the broader field of symbolic and algebraic manipulation. https://www.sciencedirect.com/science/article/pii/S0747717189800070 https://www.sciencedirect.com/science/article/pii/S074771718... https://github.com/maths/press https://github.com/maths/press I'm not trying to promote Prolog over TLA+ or anything, I've only just started with TLA+.