Skip to content

Literature

Jump to bottom
Michael Rawson edited this page Jul 12, 2023 · 1 revision

Ancient:

  • Stickel M.E. (1985) Automated deduction by theory resolution. J. Autom. Reasoning (Martin SKIMMED)

Spass+T:

  • Prevosto V., Waldmann U. (2006), SPASS+T, Sutcliffe G., Schmidt R., Schulz S., Proceedings of the FLoC'06 Workshop on Empirically Successful Computerized Reasoning (PRINTED Martin)
  • Zimmer S. (2007), Intelligent Combination of a First Order Theorem Prover and SMT Procedures, _MSc thesis, Saarland University (Saarbruecken, Germany). _

Melia:

  • Peter Baumgartner, Alexander Fuchs, Cesare Tinelli (2008), ME(LIA) - Model Evolution with Linear Integer Arithmetic Constraints. LPAR : 258-273 (PRINTED Giles)
  • Baumgartner P., Tinelli C. (2011), Model Evolution with Equality Modulo Built-in Theories, CADE (PRINTED Giles)
  • Peter Baumgartner and Uwe Waldmann (2011), A Combined Superposition and Model Evolution Calculus, J. Autom. Reasoning
  • slides from previous paper

Princess:

  • Rümmer P. (2008), A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic, LPAR (PRINTED Martin)
  • Rümmer P. (2012), E-Matching with Free Variables, LPAR (PRINTED Martin)

Hiearchical Superposition (impl. Beagle):

  • Bachmair, L., Ganzinger, H., Waldmann, U. (1994), Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput (PRINTED Martin)

  • Baumgartner P., Waldmann U. (2013), Hierarchic Superposition With Weak Abstraction, CADE (PRINTED Martin) There is also a TR

  • There are these slides

  • Baumgartner, P., Waldmann, U. (2013), Hierarchic superposition: Completeness without compactness. MACIS (PRINTED Martin)

  • Kruglov, E. (2013) Superposition Modulo Theory; dissertation

"On the other hand the hierarchic approach cannot be easily extended to deal simultaneously with several different theories outside the free part in a straight forward way as it is the case for SMT based procedures using the Nelson-Oppen method, even if queries are ground. Here further research is needed."

  • Althaus, E., Kruglov, E.,Weidenbach, C. (2009), Superposition modulo linear arithmetic SUP(LA). FroCoS
  • Kruglov, E., Weidenbach, C. (2012), Superposition decides the first-order logic fragment over ground theories. Mathematics in Computer Science

Hierarchic Reasoning in Local Theory Extensions

  • Viorica Sofronie-Stokkermans.(2005) Hierarchic reasoning in local theory extensions. CADE
  • Carsten Ihlemann, Swen Jacobs, and Viorica Sofronie-Stokkermans. (2008) On local reasoning in verification. TACAS
  • Carsten Ihlemann and Viorica Sofronie-Stokkermans. (2010) On hierarchical reasoning in combinations of theories. IJCAR

Further first order + arithmetic (either are incomplete; do not accept free BG-sorted operators at all?):

  • Korovin, K., Voronkov, A. (2007) Integrating linear arithmetic into superposition calculus. CSL (PRINTED Giles)
  • Ganzinger, H., Korovin, K. (2006) Theory instantiation, LPAR (DOWNLOADED Giles)

SMT (general):

  • Nieuwenhuis, R. and Oliveras, A. and Tinelli, C. (2006), Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T) J. ACM
  • Roberto Sebastiani. (2007) Lazy satisability modulo theories. JSAT
  • Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. (2009) Satisfiability modulo theories. In Handbook of SAT. (read Martin)

different equality sharing methods in SMT

  • Leonardo Mendonça de Moura and Nikolaj Bjørner. (2008) Model-based theory combination. Electr. Notes Theor. Comput. Sci (PRINTED Martin)

SMT with `heuristic instantiation' (E-matching?):

  • DAVID DETLEFS, GREG NELSON, AND JAMES B. SAXE (2005) Simplify: A Theorem Prover for Program Checking, J. ACM

  • Michał Moskal, et al. (2006) Fast Quantifier Reasoning With Lazy Proof Explication (TR)

  • Ge, Y., Barrett, C.W., Tinelli, C. (2007), Solving quantified verification conditions using satisfiability modulo theories. CADE (PRINTED Martin) -- there is also a journal version from 2009

  • de Moura, L., Bjørner, N.S. (2007) Efficient E-matching for SMT solvers. CADE (PRINTED Martin)

  • Ge, Y., de Moura, L. (2009) Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. CAV (PRINTED Martin)

  • (the above is inspired by) Aaron R. Bradley, Zohar Manna, and Henny B. Sipma (2006) What’s Decidable About Arrays? VMCAI

SMT + FO on top:

  • L. M. de Moura and N. Bjørner. (2008) Engineering DPLL(T) + saturation. IJCAR (PRINTED Martin)

  • A. Armando, M. P. Bonacina, S. Ranise, and S. Schulz. (2009) New results on rewrite-based satisfiability procedures (maybe rather not) ACM Trans. Comput. Log.

  • M. P. Bonacina, C. Lynch, and L. M. de Moura. (2009) On deciding satisfiability by DPLL(\Gamma+T) and unsound theorem proving. CADE

  • M. P. Bonacina, C. Lynch, and L. M. de Moura. (2011) On deciding satisfiability by theorem proving with speculative inferences (We describe a theorem-proving method that tightly integrates superposition-based inference system and SMT solver) _ J. Autom. Reasoning_ (PRINTED Martin)

(CVC4)

  • Andrew Reynolds, Cesare Tinelli, Leonardo de Moura (2014), Finding Conflicting Instances of Formulas in SMT FMCAD (PRINTED Martin)

Some finiteness restriction:

  • in Hiearchical: Peter Baumgartner and Joshua Bax and Uwe Waldmann (2014), Finite Quantification in Hierarchic Theorem Proving, IJCAR
  • in SMT (CVC4): Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic (2013), Finite Model Finding in SMT, CAV Reynolds, A., Tinelli, C., Goel, A., Krsti´c, S., Deters,M., Barrett, C. (2013) Quantifier instantiation techniques for finite model finding in SMT. CADE

Congruence closure:

  • Greg Nelson, Derek C. Oppen (1980) Fast Decision Procedures Based on Congruence Closure. J. ACM (PRINTED Martin)
  • Jean H. Gallier, Paliath Narendran, David A. Plaisted, Stan Raatz, Wayne Snyder (1993) An Algorithm for Finding Canonical Sets of Ground Rewrite Rules in Polynomial Time. J. ACM (PRINTED Martin)
  • Wayne Snyder (1993) A Fast Algorithm for Generating Reduced Ground Rewriting Systems from a Set of Ground Equations. J. Symb. Comput. (PRINTED Martin)
  • Deepak Kapur (1997) Shostak's Congruence Closure as Completion. RTA (PRINTED Giles)
  • Robert Nieuwenhuis , Albert Oliveras (2006) Fast Congruence Closure and Extensions, Inf. Comput. (PRINTED Martin)
  • Natarajan Shankar , Harald Rueß (2002) Combining Shostak Theories (PRINTED Giles)
  • Robert Nieuwenhuis , Albert Oliveras (2005) Proof-Producing Congruence Closure
Clone this wiki locally