Decision Procedures for Logical Theories

---

Schedule

---

20.10.05

Preparatory meeting

[pdf]

08.11.05

Giving talks

Uwe Waldmann

[pdf]

15.11.05 22.11.05

Introductory notions

Uwe Waldmann

Logic [v4] [v5] Resolution (propositional) [v6] [v7] Resolution (general) [v8] [v9] Equality (general) [v13] [v14] [v15]

29.11.05

Linear rational arithmetic

Ivelina Stavreva

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.

06.12.05

Abstract congruence closure

Walid Haddad

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. "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. L. Bachmair and A. Tiwari and L. Vigneron. "Abstract Congruence Closure" J. of Automated Reasoning 31(2), 2003, pp. 129--168, Kluwer Academic Publishers.

13.12.05

Superposition decision procedures for data types

Mohammed Abushammala

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. Proc. CSL 2001, LNCS 2142: 513-527

20.12.05

Combinations of theories: Introductory notions

V. Sofronie-Stokkermans

[pdf]

10.01.05

Combinations of theories over disjoint signatures

Can Kayali

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.

17.01.05

Shostak's method

Arnaud Fietzke

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

24.01.05

SAT checking modulo a theory

Patrick Wischnewski

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

31.01.05

Local theory extensions

Rayna Dimitrova

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.

07.02.05

Decision Procedures for Recursive Data Structures with Integer Constraints

Dilyana Dimova

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. D. Oppen. Reasoning about recursively defined data structures. Journal of the ACM, 27(3): 401--411.

14.02.05

Decision procedures and applications to compiler verification

Artem Starostin

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.

14.02.06

Combinations of theories: Summary

V. Sofronie-Stokkermans

[pdf]

---

Viorica Sofronie-Stokkermans <sofronie@mpi-sb.mpg.de> November 8, 2005.

---