snippetModerate
Framework or tools to generate theorem prover/solver/reasoner for new logic
Viewed 0 times
newproverlogicgeneratetheoremforreasonersolvertoolsframework
Problem
I have new logic which has syntax and semantics in usual natural languages and I have to create theorem prover/solver/reasoner for this logic. Is there framework or tool set that can generate such prover from the formal definition of grammar and semantics? I have heard about Isabelle/HOL, is this right set of tools. Is such generation a common path to proceed. Are the metalogical framework, prover compilers suitable for any kind of new logic?
Of course, I can create parser and encode all the algorithms by myself from scratch but this is not the common practice, I guess?
Of course, I can create parser and encode all the algorithms by myself from scratch but this is not the common practice, I guess?
Solution
There are many related ways you can mechanise your logic.
-
Deep embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is (almost) always possible, but makes using the embedded logic awkward.
-
Shallow embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is only possible when the embedded and embedding logics are sufficiently similar, but when it works it tends to work well.
-
Embedding into Isabelle. Note that Isabelle is a meta-tool for embedding logics, and Isabelle/HOL is but an implementation of HOL using the Isabelle tool. This is probably a lot of work, and moreover, most of the proof automation available for Isabelle/HOL is targetxing the logic HOL, so is unlikely to work for your specific logics.
-
Roll your own. It's quite easy to build a proof checker, should be just a few lines of code, especially if you take the LCF approach. More advanced tools are rather difficult, a modern SAT solver is probably > 10k LOC and that's for propositional logic, which is the simplest logic.
-
Logical frameworks. Some $\lambda$-calculi have been built particularly to enable the embedding of logics. Most well-known might be the Edinburgh Logical Framework and Pure Type Systems. Some mechanismation of those is available, but whether that is usable for you I don't know.
-
Deep embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is (almost) always possible, but makes using the embedded logic awkward.
-
Shallow embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is only possible when the embedded and embedding logics are sufficiently similar, but when it works it tends to work well.
-
Embedding into Isabelle. Note that Isabelle is a meta-tool for embedding logics, and Isabelle/HOL is but an implementation of HOL using the Isabelle tool. This is probably a lot of work, and moreover, most of the proof automation available for Isabelle/HOL is targetxing the logic HOL, so is unlikely to work for your specific logics.
-
Roll your own. It's quite easy to build a proof checker, should be just a few lines of code, especially if you take the LCF approach. More advanced tools are rather difficult, a modern SAT solver is probably > 10k LOC and that's for propositional logic, which is the simplest logic.
-
Logical frameworks. Some $\lambda$-calculi have been built particularly to enable the embedding of logics. Most well-known might be the Edinburgh Logical Framework and Pure Type Systems. Some mechanismation of those is available, but whether that is usable for you I don't know.
Context
StackExchange Computer Science Q#63604, answer score: 10
Revisions (0)
No revisions yet.