Decision Procedures for Logical Theories

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.

• 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.

• 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.

• 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.

• 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.

• 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.

• 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.

• 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.

• 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.

• 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.