6
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ questions regarding programming tools are off-topic here. $\endgroup$ – sashas Sep 18 '16 at 12:51
  • $\begingroup$ @sasha I don't think the essence of the question is about tools, but about logics. $\endgroup$ – Martin Berger Sep 18 '16 at 14:04
  • 1
    $\begingroup$ @MartinBerger my bad. $\endgroup$ – sashas Sep 18 '16 at 14:35
10
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ Another approach would be using a logic programming language such as Prolog. In particular if you have a suitable proof system, proof search can be very quickly implemented. $\endgroup$ – godfatherofpolka Sep 19 '16 at 5:22
  • 2
    $\begingroup$ I would recommend as a first try a tool for logical frameworks. You can use Twelf or Abella, I'd recommend Abella. We recently switchted to it from Twelf for working with logics for programming languages, and we're happier now. $\endgroup$ – Andrej Bauer Sep 19 '16 at 6:21
  • 1
    $\begingroup$ @godfatherofpolka I agree, logic programming is another option that I had forgotten about. $\endgroup$ – Martin Berger Sep 19 '16 at 6:50
  • 2
    $\begingroup$ @AndrejBauer I have no personal experience with Abella, happy to believe it's more usable than Twelf. What kind of automation does Abella offer? $\endgroup$ – Martin Berger Sep 19 '16 at 6:51
  • 2
    $\begingroup$ It's interactive, which helps a lot. And it performs "auto-like" proof search, while in Twelf you have to do everything with your bare hands. $\endgroup$ – Andrej Bauer Sep 19 '16 at 13:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.