Ackermann's book "Solvable Cases of the Decision Problem" discusses decidable instances of first order logic, particularly monadic logic, and so called "equality formulas". However, the book is from 1954, the notation is terse, full of German letters, and presented in a very non-algorithmic way (which is unsurprising, given the time). I'm having some trouble reading it.

Have any papers given the results from the book in a more modern presentation? Perhaps using modern inference-rules, pseudocode for algorithms, and better typesetting? I'm particularly interested in the section on monadic logic, since other references I have found have described it as "implementable in practice", despite giving no clues as to why this is true.

  • 1
    $\begingroup$ You should definitely have a look at the "Classical Decision Problem" by Boerger, Graedel and Gurevich, the BGG. $\endgroup$ – Dmitri Chubarov Nov 13 '17 at 4:04
  • 1
    $\begingroup$ Another more recent reference is the "Handbook of Practical Logic and Automated Reasoning" by John Harrison. This comes with an OCaml implementation of the decision procedure based on the finite model property. $\endgroup$ – Dmitri Chubarov Nov 13 '17 at 4:15
  • $\begingroup$ @DmitriChubarov If you put these in an answer, I'll accept it $\endgroup$ – jmite Nov 20 '17 at 20:08

Your Answer

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

Browse other questions tagged or ask your own question.