4 ms·

Disclaimer: My knowledge on this topic is not in depth (as I said, I'm still learning). I haven't heard of Z3 but it says it's a theorem prover, so it would be

by fizixer 10y ago

Disclaimer: My knowledge on this topic is not in depth (as I said, I'm still learning). I haven't heard of Z3 but it says it's a theorem prover, so it would be comparable to systems like Coq, Isabelle, which are also considered programming languages, and then compared to Agda, Idris, and, last but not the least, Haskell. So a distilled form of your question would be: - How does logic programming compare to pure functional programming and programming based on type theory? For that I would probably try to read the following [1] before spending more time on it. - How does Prolog compare to Haskell? For this I'd probably look at something like this [2] I'm not too well-versed in the SML/OCaml/Haskell arena, but if I have to venture a guess, if we try to build a complex GOFAI system in prolog vs in haskell, the prolog system would have less amount of prolog code and most of the complexity would reside in the database of facts, whereas in haskell, all/most of the complexity would manifest in the form of haskell code. Another difference would be that a logic programming system comes with a general purpose inference engine and you can build any expert system using it, but you have to provide the relevant knowledge base. Whereas Haskell comes with a custom-built inference engine (the Hindley-Milner type inference) that only knows about types (if you need to build an expert system in Haskell, you would first build a general purpose inference engine, and essentially a prolog-like system, before you do anything else). On the flip side, Prolog program interpretation mechanism would probably be considered ad hoc, whereas Haskell program interpretation is based on type theory. So a Haskell programmer would probably have to worry less about program correctness. [1] http://stackoverflow.com/questions/8297574 http://stackoverflow.com/questions/8297574 [2] http://stackoverflow.com/questions/1932770 http://stackoverflow.com/questions/1932770 EDIT: And theorem proving also connects to areas of model checking, specification languages, as well as compiler backend areas like operational/denotational semantics. Like I said it's a tangled web of many core CS areas. EDIT 2: On further reading, Z3 is listed on this wikipedia page [3] as a constraint-programming (CP) library for an imperative language. The contrast between CP and CLP is mentioned on that page (as well as both Z3 and Prolog). (that also means Z3 is not really comparable to Coq, Isabelle as I said earlier. Coq, Isabelle are interactive theorem provers or proof assistants, not automatic theorem provers which is a lot harder to do). Another useful discussion [4] [3] https://en.wikipedia.org/wiki/Constraint_programming https://en.wikipedia.org/wiki/Constraint_programming [4] http://cs.stackexchange.com/questions/14946 http://cs.stackexchange.com/questions/14946

ScottBurson 10y ago
> Coq, Isabelle are interactive theorem provers or proof assistants, not automatic theorem provers which is a lot harder to do Automatic theorem provers for first-order logic (FOL) have existed for some time [0], but higher-order logic (HOL) is another matter. The difference is that in HOL, predicates can be variables; in FOL they are all constants. HOL allows you to write rules for mathematical induction; for example: ∀P P(0) ∧ (∀n n ≥ 0 ∧ P(n) ⇒ P(n + 1)) ⇒ (∀n n ≥ 0 ⇒ P(n)) This says that for any predicate P on the natural numbers, if you can show, first, that P(0), and second, that for any natural n, P(n) implies P(n + 1), then you can conclude that P is true for any n. This rule is not a valid FOL statement, because it starts off quantifying over possible predicates, which is not permitted in FOL. Reasoning of this kind, although usually informal, is necessary for programmers to understand any iterative or recursive piece of code. To understand such code, you have to know what invariant it maintains; proofs of such invariants are always inductive. So HOL is required, in most cases, for formal verification of software. But no one has figured out how to build an automated prover for HOL. My own theory as to why is simply that the branching factor is higher. It's like the difference between chess and Go: the branching factor -- the average number of possible moves from any board position -- is small enough in chess that brute-force search can be sufficient to play at a world level, at least in the mid- and end-game; but in Go, it's much larger, so that brute-force search doesn't get you very far. As you say, lacking a fully automated HOL prover, people have been using proof assistants instead. These keep track of the details of the proof, which is still a very useful function, and can perform certain simple deductive steps themselves, but require manual intervention at certain critical points, such as the introduction of induction hypotheses. [0] https://en.wikipedia.org/wiki/Automated_theorem_proving https://en.wikipedia.org/wiki/Automated_theorem_proving
- c-cube 10y ago
  There are some automated theorem provers for higher-order logic [0][1], but they are not very good yet compared to their first-order counterpart. There are also some provers specialized in inductive proofs [2][3], although the frontier with proof assistants such as Coq or Isabelle starts getting blurry as you often need the user's intervention to explicitely provide lemmas. I have some hopes that this is going to change in the next few years thanks to a colleague's effort [4] to build better higher-order provers. He's an expert in Sledgehammer (a tool to use automated provers from Isabelle) which is already a productivity boost, and should become better with this project. You are right that the search space is more difficult to handle. Induction (and similar formulas) is particularly hard to handle because one usually has to introduce lemmas, and these lemmas have to be "guessed" (infinite branching factor there). Existing provers basically rely on heuristics to try and find lemmas that would be useful for solving the current goal(s). ACL2 [3] for instance uses heuristics accumulated and refined for decades. Hopefully, proof assistants will get tighter and tighter integration with automated provers, and the user will have to specify only the main lemmas and the overall shape of a proof, leaving the details to CPU crunching. [0] https://page.mi.fu-berlin.de/cbenzmueller/leo/ https://page.mi.fu-berlin.de/cbenzmueller/leo/ [1] https://www.ps.uni-saarland.de/~cebrown/satallax/ https://www.ps.uni-saarland.de/~cebrown/satallax/ [2] https://github.com/sorinica/spike-prover https://github.com/sorinica/spike-prover [3] https://www.cs.utexas.edu/users/moore/acl2/ https://www.cs.utexas.edu/users/moore/acl2/ [4] http://matryoshka.gforge.inria.fr/ http://matryoshka.gforge.inria.fr/

by fizixer 10y ago

ScottBurson 10y ago

> Coq, Isabelle are interactive theorem provers or proof assistants, not automatic theorem provers which is a lot harder to do Automatic theorem provers for first-order logic (FOL) have existed for some time [0], but higher-order logic (HOL) is another matter. The difference is that in HOL, predicates can be variables; in FOL they are all constants. HOL allows you to write rules for mathematical induction; for example: ∀P P(0) ∧ (∀n n ≥ 0 ∧ P(n) ⇒ P(n + 1)) ⇒ (∀n n ≥ 0 ⇒ P(n)) This says that for any predicate P on the natural numbers, if you can show, first, that P(0), and second, that for any natural n, P(n) implies P(n + 1), then you can conclude that P is true for any n. This rule is not a valid FOL statement, because it starts off quantifying over possible predicates, which is not permitted in FOL. Reasoning of this kind, although usually informal, is necessary for programmers to understand any iterative or recursive piece of code. To understand such code, you have to know what invariant it maintains; proofs of such invariants are always inductive. So HOL is required, in most cases, for formal verification of software. But no one has figured out how to build an automated prover for HOL. My own theory as to why is simply that the branching factor is higher. It's like the difference between chess and Go: the branching factor -- the average number of possible moves from any board position -- is small enough in chess that brute-force search can be sufficient to play at a world level, at least in the mid- and end-game; but in Go, it's much larger, so that brute-force search doesn't get you very far. As you say, lacking a fully automated HOL prover, people have been using proof assistants instead. These keep track of the details of the proof, which is still a very useful function, and can perform certain simple deductive steps themselves, but require manual intervention at certain critical points, such as the introduction of induction hypotheses. [0] https://en.wikipedia.org/wiki/Automated_theorem_proving https://en.wikipedia.org/wiki/Automated_theorem_proving

c-cube 10y ago
There are some automated theorem provers for higher-order logic [0][1], but they are not very good yet compared to their first-order counterpart. There are also some provers specialized in inductive proofs [2][3], although the frontier with proof assistants such as Coq or Isabelle starts getting blurry as you often need the user's intervention to explicitely provide lemmas. I have some hopes that this is going to change in the next few years thanks to a colleague's effort [4] to build better higher-order provers. He's an expert in Sledgehammer (a tool to use automated provers from Isabelle) which is already a productivity boost, and should become better with this project. You are right that the search space is more difficult to handle. Induction (and similar formulas) is particularly hard to handle because one usually has to introduce lemmas, and these lemmas have to be "guessed" (infinite branching factor there). Existing provers basically rely on heuristics to try and find lemmas that would be useful for solving the current goal(s). ACL2 [3] for instance uses heuristics accumulated and refined for decades. Hopefully, proof assistants will get tighter and tighter integration with automated provers, and the user will have to specify only the main lemmas and the overall shape of a proof, leaving the details to CPU crunching. [0] https://page.mi.fu-berlin.de/cbenzmueller/leo/ https://page.mi.fu-berlin.de/cbenzmueller/leo/ [1] https://www.ps.uni-saarland.de/~cebrown/satallax/ https://www.ps.uni-saarland.de/~cebrown/satallax/ [2] https://github.com/sorinica/spike-prover https://github.com/sorinica/spike-prover [3] https://www.cs.utexas.edu/users/moore/acl2/ https://www.cs.utexas.edu/users/moore/acl2/ [4] http://matryoshka.gforge.inria.fr/ http://matryoshka.gforge.inria.fr/