[an error occurred while processing this directive]

Thomas Hillenbrand

[an error occurred while processing this directive]

Decision Procedures for Logical Theories

Seminar Winter 2001/02

Harald Ganzinger | Uwe Waldmann | Thomas Hillenbrand

General logical formalisms such as predicate logic, set theory, or number theory are undecidable or even not recursively enumerable. However, such generality is not needed in all applications: Important special cases such as the theory of integers with addition are decidable, as well as the theory of lists or of arrays. For computer-aided reasoning, it is vital to combine general deductive mechanisms like resolution with decision procedures for special structures in order to succeed in the respective application areas. Substantially more properties can then be proved automatically. Thus the practical applicability of corresponding tools (e.g. for verification) is improved considerably.

In the seminar fundamental methods for the construction of decision procedures have been discussed. One may distinguish semantical methods, quasi-semantical methods and proof-theoretical ones; a further source is automata theory. Finally, the question has been considered how and under which conditions such special procedures can be combined and integrated into more general ones.

Three seminar sessions have been held from December 01 until February 02. If you have further questions regarding the seminar, please contact Thomas Hillenbrand.

List of Topics

Abstract Congruence Closure | Superposition-Based Decision Procedures | Fischer-Ladner Closure | Ordered Resolution | Guarded Fragment | Automata Theory for Presburger Arithmetic | Rabin Automata | Finite Model Property | Combinations of Decision Procedures

Debapriyo Majumdar

Abstract Congruence Closure


  • L. Bachmair and A. Tiwari. Abstract congruence closure and specializations. In D.A. McAllester, editor, Proceedings of the 17th International Conference on Automated Deduction, volume 1831 of LNAI, pages 64-78. Springer-Verlag, 2000.
  • G. Nelson and D.C. Oppen. Fast decision procedures based on congruence closure. Journal of the ACM, 27(2):356-364, 1980.

Yevgeny Kazakov

Superposition-Based Decision Procedures



  • A. Armando, S. Ranise, and M. Rusinowitch. Uniform derivation of decision procedures by superposition. In L. Fribourg, editor, Proceedings of the 15th International Workshop on Computer Science Logic, volume 2142 of LNCS, pages 513-527. Springer-Verlag, 2001.

Harald Ganzinger

Fischer-Ladner Closure

  • M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194-211, 1979.
  • E.A. Emerson and A.P. Sistla. Deciding full branching time logic. Information and Control, 61(3):175-201, 1984.

Atika Mustafa

Ordered Resolution



  • C.G. Fermüller, A. Leitsch, U. Hustadt, and T. Tammet. Resolution decision procedures. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume II, chapter 25, pages 1791-1849. Elsevier Science Publishers, 2001.
  • W.H. Joyner Jr. Resolution. Strategies as Decision Procedures. Journal of the ACM, 23(3):398-417, 1976.

Syed Fawad Mustafa

Guarded Fragment



  • H. Ganzinger and H. de Nivelle. A superposition decision procedure for the guarded fragment with equality. In Proceedings of the 14th IEEE Symposium on Logic in Computer Science, pages 295-305. IEEE Computer Society Press, 1999.

Masood Obaid

Automata Theory for Presburger Arithmetic



  • J.E. Hopcroft and J.D. Ullmann. Introduction to Automata Theory, Languages, and Computation, chapter 2: Finite automata and regular expressions, pages 13-54. Addison-Wesley, 1979.
  • H. Comon and C. Kirchner. Presburger arithmetic and classical word automata. In H. Comon, C. Marché and R. Treinen, editors, Constraints in Computational Logic: Theory and Applications, volume 2002 of LNCS, chapter 2: Constraint solving on terms, section 8, pages 79-83. Springer-Verlag, 1999.

Hans de Nivelle

Rabin Automata

  • W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume 3: Beyond Words, chapter 7, pages 389-455. Springer-Verlag, 1997.

Irena Galic

Finite Model Property


  • E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem, chapter 6: Standard classes with the finite model property, pages 239-313. Springer-Verlag, 1997.

Viorica Sofronie-Stokkermans

Combinations of Decision Procedures



  • G. Nelson and D.C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):243-257, 1979.
  • F. Baader and K.U. Schulz. Unification in the union of disjoint equational theories: combining decision procedures. Journal of Symbolic Computation, 21(2):211-243, 1996.


[an error occurred while processing this directive]
This web page is maintained by Thomas Hillenbrand <hillen@mpi-sb.mpg.de>.
Imprint / Impressum | Data Protection / Datenschutzhinweis
Document last modified on Wednesday, 12-Jun-2002 13:37:15 CEST.