Readings

Background

[Hod95] Short Model Theory Course
by W. Hodges. Lecture Notes, Johannesburg, 1995

[Ohl97] Introductory Logic Course
by H. J. Ohlbach. Lecture Notes, Imperial College, London, 1997 (see also related slides).

[Sti87] An introduction to automated deduction
by Mark. E. Stickel. In W. Bibel and P. Jorrand editors, Fundamentals of Artificial Intelligence, Vol 232 of Lecture Notes in Computer Science, Springer, 1987

[EisOhl93] Deduction systems based on resolution
by N. Eisinger and H. J. Ohlbach. In J. A. Robinson et al. editors, Handbook of Logic in Artificial Intelligence and Logic Programming vol. 1 Oxford University Press, 1993.

[Hen00] An Introduction to Prolog Programming
by Ulle Hendris. Lecture Notes, King's College, London, 2000.

[Lei97] The Resolution Calculus
by Alexander Leitsch. Texts in Theoretical Computer Science, An EATCS Series, Springer, 1997.

[SocJoh97] Deduction Systems
by Rolf Socher-Ambrosius and Patricia Johann. Graduate Texts in Computer Science, Springer, 1997.

[ChaLee73] Symbolic Logic and Mechanical Theorem Proving
by Chin-Liang Chang and Richard Char-Tung Lee. Computer Science Classics, Academic Press, 1973.

[Ram89] Formal Methods in Artificial Intelligence.
by Allan Ramsay. Cambridge Tracts in Theoretical Computer Science 6, Cambridge University Press, 1989.

Class Readings

Theory Reasoning

[Sti85] Automated Deduction by Theory Resolution
by Mark E. Stickel. Journal of Automated Reasoning, vol. 1(4), 1985.

[Bau92a] An Ordered Theory Resolution Calculus
by Peter Baumgartner. In A. Voronkov, editor, Logic Programming and Automated Reasoning (Proceedings), volume 624 of Lecture Notes in Artificial Intelligence, St. Petersburg, Russia, Springer, 1992.

[Bau92b] A Model Elimination Calculus with Built-in Theories
by Peter Baumgartner. In H.-J. Ohlbach, editor, Proceedings of the 16th German Workshop on Artificial Intelligence, volume 671 of Lecture Notes in Artificial Intelligence, Springer, 1992.

[Bau92c] A Unified Approach to Theory Reasoning
by Peter Baumgartner et al. Fachberichte Informatik 15/92, UniversitM-dt Koblenz-Landau, Institut fM-|r Informatik, Rheinau 1, D-56075 Koblenz, 1992.

[Bec96] Incremental theory reasoning methods for semantic tableaux.
by Bernhard Beckert and Christian Pape. In Proceedings of the 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, volume 1071 of Lecture Notes in Computer Science, Springer, 1996.

Constrained Resolution

[Bur90] A resolution principle for clauses with constrains
by Hans-Jürgen Bürckert. In Proceedings of the International Conference on Automated Deduction, vol. 449 of Lecture Notes in Artificial Intelligence, Springer, 1990.

[Fri91] The substitutional framework for sorted deduction: fundamental results on hybrid reasoning
by Alan M. Frisch, Artificial Intelligence (49)1-3, 1991.

[Bur94] A resolution principle for constrained logics
by Hans-Jürgen Bürckert. Artificial Intelligence 66, 235-271, 1994.

[Wan95] A typed resolution principle for deduction with conditional typing theory
by Tie-Cheng Wang. Artificial Intelligence 75, 161-194, 1995.

[Baa99] Using Decision Procedures to Accelerate Domain-Specific Deductive Synthesis Systems
by Jeffrey Van Baalen and Steven Roach. In P. Flener, editor, Proceedings of the 8th International Workshop on Logic Programming Synthesis and Transformation (LOPSTR'98), volume 1559 of Lecture Notes in Computer Science, Springer, 1999.

Constraint Logic Programming

[Fru93] Constraint Logic Programming - An Informal Introduction
by Thom Frühwirth et al. Technical Report ECRC-93-5, 1993.

[JafMah94] Constraint Logic Programming: a Survey
by J. Jaffar and M. Maher, Journal of Logic Programming, Special 10th Anniversary Issue, Vols 19/20, 1994. Also in Handbook of Artificial Intelligence and Logic Programming, Oxford Univ. Press, 1995.

[TinHar98] Constraint Logic Programming over Unions of Constraint Theories
by C. Tinelli and M. Harandi, The Journal of Functional and Logic Programming (6), 1998.

Constraint Rewriting

[ArmRan98] Constraint contextual rewriting
by Alessandro Armando and Silvio Ranise. In R. Caferra and G. Salzer, editors, Proceedings of the 2nd International Workshop on First Order Theorem Proving, FTP'98, Vienna (Austria), November 1998.

[ArmRan00] Termination of Constraint Contextual Rewriting
by Alessandro Armando and Silvio Ranise. In Proceedings of the 3rd International Workshop on Frontiers of Combining Systems (FroCoS'2000). Nancy (France), March 22-24, 2000.

Combination of Satisfiability Procedures

[BaaSch95] Combination of Constraint Solving Techniques: An Algebraic Point of View
by F. Baader and K.U. Schulz. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Artificial Intelligence, 1995. Springer Verlag.

[BaaTin0?] Deciding the Word Problem in the Union of Equational Theories
by Franz Baader and Cesare Tinelli. Information and Computation, 200?

[Bar96] Validity checking for combinations of theories with equality
by Clark W. Barrett et al. In M. K. Srivas and A. Camilleri,editors, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (Palo Alto, CA), volume 1166 of Lecture Notes in Computer Science, Springer, 1996

[Bar00] A framework for cooperating decision procedures
by Clark W. Barrett et al. In D. A. McAllester, editor, Proceedings of the 17th International Conference on Automated Deduction (Pittsburgh, PA), volume 1831 of Lecture Notes in Artificial Intelligence, Springer, 2000.

[Cyl96] On Shostak's decision procedure for combinations of theories
by David Cyrluk et al. In M. A. McRobbie and J.K. Slaney, editors, Proceedings of the 13th International Conference on Automated Deduction, volume 1104 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1996.

[TinHar96] A New Correctness Proof of the Nelson-Oppen Combination Procedure
by C. Tinelli and M. Harandi. Proceedings of the 1st International Workshop ``Frontiers of Combining Systems'', 1996.

Last Updated: Apr 22, 2001