Focus of the seminar:

Decidable theories:
Decision procedures for data types such as lists, arrays, ...
Decision procedures for numeric domains
Combinations of decision procedures

Methods for proving decidability:

Finite model property
Quantifier elimination
Automata theory
Resolution as a decision procedure

Applications: especially verification (but also knowledge representation or mathematics)

Suggested Topics

Decision procedures for data types

1. Reasoning about uninterpreted function symbols; congruence closure

Literature:

  • G. Nelson and D.C. Oppen. Fast decision procedures based on congruence closure. Journal of the ACM, 27(2):356-364, 1980.

  • L. Bachmair and A. Tiwari and L. Vigneron. "Abstract Congruence Closure" J. of Automated Reasoning 31(2), 2003, pp. 129--168, Kluwer Academic Publishers.

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

    • 2. Decision procedures for classical data types such as lists, arrays, ...

    Literature:

  • Alessandro Armando, Silvio Ranise, Michaël Rusinowitch. A rewriting approach to satisfiability procedures. Inf. Comput. 183(2): 140-164 (2003)

  • Alessandro Armando, Silvio Ranise, Michaël Rusinowitch. Uniform Derivation of Decision Procedures by Superposition. CSL 2001: 513-527

    • Decision procedures for numeric domains
    3. Linear rational arithmetic: The test point method vs. Fourier-Motzkin

    Literature:

  • H. Kuhn. Solvability and consistency for linear equations and inequalities. American Mathematical Monthly, 63:217M--232, 1956.

  • R. Loos and V. Weispfenning. Applying Linear Quantifier Elimination. The Computer Journal, 36(5):450-461, 1993.

  • J.-L. Lassez and M.J. Maher. On Fourier's Algorithm for Linear Arithmetic Constraints. Journal of Automated Reasoning 9: 373-379, 1992.
    • 4. Linear integer (Presburger) arithmetic: The automata-theoretic method

    Literature:

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

    • Combinations of decision procedures
    5. Combinations of theories over disjoint signatures

    Literature:

  • G. Nelson and D.C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):243-257, 1979.

  • Derek C. Oppen. Complexity, Convexity and Combinations of Theories. Theor. Comput. Sci. 12: 291-302, 1980.

  • C. Tinelli and M. Harandi. A new correctness proof of the Nelson-Oppen combination procedure.
    Proceedings FroCos'96.

  • Recent results refine the combination method.

    • 6. Combinations of theories over non-disjoint signatures

    Literature:

  • S. Ghilardi. Model Theoretic Methods in Combined Constraint Satisfiability. Journal of Automated Reasoning, vol. 33, no. 3-4, pp.221-249 (2005).

    • Reasoning in theory extensions

    7. Local theory extensions

    Literature:

  • S. Burris Polynomial time uniform word problems. Math. Logic Quarterly 41 (1995), 173 - 182.

  • H. Ganzinger. Relating Semantic and Proof-Theoretic Concepts for Polynomial Time Decidability. Proc. 16th IEEE Symposium on Logic in Computer Science, pages 81--92, IEEE Computer Society Press, 2001.

  • Viorica Sofronie-Stokkermans. Hierarchic reasoning in local theory extensions. Proceedings of the 20th International Conference on Automated Deduction (CADE 2005), (R. Nieuwenhuis, ed.), LNAI 3632, pages 219-234, Springer Verlag, 2005.

    • Several recent results on applications to verification

    8. Shostak's method

    Literature:

  • R. E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1--12, January 1984.

  • Harald Ganzinger. Shostak Light. CADE 2002: 332-346

  • Sava Krstic, Sylvain Conchon. Canonization for Disjoint Unions of Theories. CADE 2003: 197-211

    • Reasoning about complex data types

    9. Instantiation-based decision procedures for theories of arrays.

    Literature:

  • A. Bradley, Z. Manna, H. Sipma. What's decidable about arrays? Proceedings VMCAI 2006.
  • C. Ihlemann, S. Jacobs, V. Sofronie-Stokkermans. On local reasoning in verification, Proceedings TACAS 2008.
    • 10. Decision procedures for recursive data structures with integer constraints

    Literature:

  • T. Zhang, H.B. Sipma, Z. Manna. Decision Procedures for Recursive Data Structures with Integer Constraints. Proceedings of IJCAR'04, LNAI 3097, pages 152-167.

    • SAT checking modulo a theory

    11. DPLL(T)

    Literature:

  • Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli. DPLL( T): Fast Decision Procedures . CAV 2004: 175-188

  • Robert Nieuwenhuis, Albert Oliveras and Cesare Tinelli. Abstract DPLL and Abstract DPLL Modulo Theories. 11th Int. Conf. on Logics for Programming, AI and Reasoning (LPAR) Montevideo, March 2005. Springer LNAI 3452, pp 36-50.

  • Robert Nieuwenhuis, Albert Oliveras. DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. CAV 2005: 321-334

    • Interpolation

    12.Interpolation in extensions of linear arithmetic with free functions

    Literature:

  • K. McMillan. An interpolating theorem prover. Theoretical Computer Science, 2005.
  • A. Rybalchenko, V.Sofronie-Stokkermans. Constraint solving for interpolation, VMCAI 2006.
  • A. Cimatti, A. Griggio, R. Sebastiani. Efficient Interpolant Generation in Satisfiability Modulo Theories, Proc. TACAS 2008.

  • G. Yorsh, M. Musuvathi. A Combination Method for Generating Interpolants. Proc. CADE 2005.
  • V.Sofronie-Stokkermans. Interpolation in local theory extensions. Proc. IJCAR 2006.

    • Applications to verification

    13. Bounded model checking, Invariant checking

    Literature:

  • Carsten Ihlemann, Swen Jacobs, Viorica Sofronie-Stokkermans: On local reasoning in verification, Proceedings TACAS 2008.
  • Leonardo de Moura, Harald Rueß, and Maria Sorea. Lazy Theorem Proving for Bounded Model Checking over Infinite Domains Proceedings of CADE 18, LNCS 2392, pages 438--455, 2002.

    • 14. Verification by abstraction/refinement

    Literature:

  • Ken McMillan. Application of Craig interpolation in model checking, Proc. TACAS 2005.

    • Applications to knowledge representation

    Various possible topics on modal logics, description logics; combinations of modal logics; distributed databases:

    15. Decidability of the modal logic: finite model property

    Literature:

  • Graedel, Kolaitis, Linkin, Marx, Spencer, Vardi, Venema, Weinstein: Finite model theory and applications. Chapter 7. Springer 2007.

  • M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194-211, 1979.

    • 16. Resolution-based decision procedure for K

    Literature:

  • Hans Jürgen Ohlbach, Andreas Nonnengart, Maarten de Rijke and Dov Gabbay Encoding two-valued non-classical logics in classical logic, Handbook of Automated Reasoning, Vol 2, Chapter 21. 2001. (only a part of this article is needed) [PDF]

    • 17. The guarded fragment of first order logic and applications to knowledge representation

    Literature:

  • 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. [PDF]

    • 18. Decidability results for description logics: The description logic EL

    Literature:

  • Franz Baader. Terminological Cycles in a Description Logic with Existential Restrictions. In Georg Gottlob and Toby Walsh, editors, Proceedings of the 18th International Joint Conference on Artificial Intelligence, Morgan Kaufmann, 2003.
  • F. Baader, C. Lutz, B. Suntisrivaraporn. Is Tractable Reasoning in Extensions of the Description Logic EL Useful in Prectice?; Journal of Logic, Language and Information (M4M special issue); 2007.

    • (there are several other subjects on decidability results for description logics)

    19. Reasoning in combinations of modal logics

    Literature:

  • S. Ghilardi, L. Santocanale Algebraic and Model-Theoretic Techniques for Fusion Decidability in Modal Logic, in Vardi M., Voronkov A. Logic for Programming, Artificial Intelligence and Reasoning (LPAR 03), Springer LNAI, vol.2850, pp.152-166 (2003). [PDF]
    • related to topic 6.

    20. Reasoning in extensions/combinations/fusions of description logics

    Literature:

  • Several papers by Baader/Ghilardi/Lutz/Wolter/...