Suggested topics

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

Tractable fragments of first-order logic; methods for recognizing tractability

Applications: verification, knowledge representation, mathematics

Suggested Topics

Decision procedures for data types

1. Reasoning about uninterpreted function symbols; congruence closure

Literature:

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

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

    • 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 and linear integer (Presburger) arithmetic: The Fourier-Motzkin algorithm and the Omega test

    Literature:

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

  • W. Pugh. A practical algorithm for exact array dependence analysis. Commun. ACM, 35(8):102M--115, August 1992.

  • 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 rational arithmetic: The test point method

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

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

    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

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

    • link with 2, 16.

    10. SAT checking modulo a theory

    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

    • Methods for proving decidability

    (can be also integrated with the topics mentioned above)

    11. Finite model property

    Literature:

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

    • 12. Quantifier elimination

    Literature:

  • H.B. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972.

    • 13. An application of quantifier elimination

    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.

    • Note: Link with 4 and 5. Also links with QE for acyclic datastructures.

    14. Resolution as a decision procedure

    Literature:

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

    • Tractability; methods for recognizing tractability
    15. Local theories (syntactic aspects)

    Literature:

  • D. McAllester, R. Givan. Polynomial Time Computation via Local Inference Relations. ACM TOCL 3(4): 521-541 (2002).

    • (also useful:

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

    Links with 2, 10.

    Applications:

     Note: below only verification;

    (additional topics: knowledge representation, mathematics)

    16. Bounded model checking

    Literature:

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

    • (may also be of interest:

  • Martin Fränzle and Christian Herde. Efficient proof engines for bounded model checking of hybrid systems. In Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 04), Electronic Notes in Theoretical Computer Science (ENTCS). Elsevier, 2004.

    • )

    17. Compiler verification

    Literature:

  • A. Pnueli and O. Shtrichman and M. Siegel. The code validation tool (CVT): Automatic verification of a compilation process. STTT 2(2): 192-201 (1998).

  • Leonore Zuck, Amir Pnueli, Benjamin Goldberg, Clark Barrett, Yi Fang, and Ying Hu. Translation and Run-Time Validation of Loop Tranformations. To Appear in Journal of Formal Methods in System Design. November 2005.

    • Additional Topics

  • UCLID
  • Robust constraint solving
  • Fischer-Ladner Closure
  • The guarded fragment of first order logic and applications to knowledge representation
  • Monadic second order logic
  • Automated reasoning in mathematics
  • ....