7
$\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?

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

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
5
  • 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
    Commented Sep 19, 2016 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
    Commented Sep 19, 2016 at 6:21
  • 1
    $\begingroup$ @godfatherofpolka I agree, logic programming is another option that I had forgotten about. $\endgroup$
    – Martin Berger
    Commented Sep 19, 2016 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
    Commented Sep 19, 2016 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
    Commented Sep 19, 2016 at 13:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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