References

  1. Gábor Alagi & Christoph Weidenbach (2015): NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment. In: Carsten Lutz & Silvio Ranise: Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings, Lecture Notes in Computer Science 9322. Springer, pp. 69–84, doi:10.1007/978-3-319-24246-0_5.
  2. Leo Bachmair & Harald Ganzinger (1994): Rewrite-based Equational Theorem Proving with Selection and Simplification. Journal of Logic and Computation 4(3), pp. 217–247, doi:10.1093/logcom/4.3.217. Revised version of Max-Planck-Institut für Informatik technical report, MPI-I-91-208, 1991.
  3. Leo Bachmair & Harald Ganzinger (2001): Resolution Theorem Proving. In: Alan Robinson & Andrei Voronkov: Handbook of Automated Reasoning, chapter 2 I. Elsevier, pp. 19–99, doi:10.1016/B978-044450813-3/50004-7.
  4. Peter Baumgartner, Alexander Fuchs & Cesare Tinelli (2006): Lemma Learning in the Model Evolution Calculus. In: LPAR, Lecture Notes in Computer Science 4246. Springer, pp. 572–586, doi:10.1016/0004-3702(94)90077-9.
  5. Paul Bernays & Moses Schönfinkel (1928): Zum Entscheidungsproblem der mathematischen Logik. Mathematische Annalen 99, pp. 342–372, doi:10.1007/BF014591101.
  6. Armin Biere, Marijn Heule, Hans van Maaren & Toby Walsh (2009): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications 185. IOS Press.
  7. Jasmin Christian Blanchette, Mathias Fleury & Christoph Weidenbach (2016): A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality. In: Nicola Olivetti & Ashish Tiwari: Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, Lecture Notes in Computer Science 9706. Springer, pp. 25–44, doi:10.1007/978-3-319-43144-4.
  8. Maria Paola Bonacina & David A. Plaisted (2016): Semantically-Guided Goal-Sensitive Reasoning: Model Representation. Journal of Automated Reasoning 56(2), pp. 113–141, doi:10.1007/s10817-015-9334-4.
  9. Aaron R. Bradley & Zohar Manna (2007): The Calculus of Computation – Decision Procedures with Applications to Verification. Springer, doi:10.1007/978-3-540-74113-8.
  10. Martin Bromberger (2018): A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems. In: Didier Galmiche, Stephan Schulz & Roberto Sebastiani: Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Lecture Notes in Computer Science 10900. Springer, pp. 329–345, doi:10.1145/322276.322287.
  11. Martin Bromberger, Thomas Sturm & Christoph Weidenbach (2015): Linear Integer Arithmetic Revisited. In: Amy P. Felty & Aart Middeldorp: Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, Lecture Notes in Computer Science 9195. Springer, pp. 623–637, doi:10.1016/S0747-7171(08)80051-X.
  12. Martin Bromberger & Christoph Weidenbach (2017): New techniques for linear arithmetic: cubes and equalities. Formal Methods in System Design 51(3), pp. 433–461, doi:10.1007/s10703-017-0278-7.
  13. Christian G. Fermüller & Reinhard Pichler (2007): Model Representation over Finite and Infinite Signatures. J. Log. Comput. 17(3), pp. 453–477, doi:10.1093/logcom/exm008.
  14. Alberto Fiori & Christoph Weidenbach (2019): SCL – Clause Learning from Simple Models. In: Automated Deduction - CADE-27, 27th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 11716. Springer, pp. 233–249, doi:10.1007/978-3-030-29436-6_14.
  15. Harald Ganzinger & Konstantin Korovin (2003): New Directions in Instatiation–Based Theorem Proving. In: Samson Abramsky: 18th Annual IEEE Symposium on Logic in Computer Science, LICS'03, LICS'03. IEEE Computer Society, pp. 55–64, doi:10.1109/LICS.2003.1210045.
  16. Marijn J. H. Heule, Benjamin Kiesl & Armin Biere (2019): Encoding Redundancy for Satisfaction-Driven Clause Learning. In: Tomás Vojnar & Lijun Zhang: Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, Lecture Notes in Computer Science 11427. Springer, pp. 41–58, doi:10.1007/978-3-030-17462-0.
  17. Richard M. Karp (1972): Reducibility Among Combinatorial Problems. In: Raymond E. Miller & James W. Thatcher: Proceedings of a symposium on the Complexity of Computer Computations, held March 20-22, 1972, at the IBM Thomas J. Watson Research Center, Yorktown Heights, New York., The IBM Research Symposia Series. Plenum Press, New York, pp. 85–103, doi:10.1007/978-1-4684-2001-2_9.
  18. Daniel Kroening & Ofer Strichman (2008): Decision Procedures An Algorithmic Point of View. Texts in Theoretical Computer Science. Springer. Second Edition 2016.
  19. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang & Sharad Malik (2001): Chaff: Engineering an Efficient SAT Solver. In: Design Automation Conference, 2001. Proceedings. ACM, pp. 530–535, doi:10.1145/378239.379017.
  20. Robert Nieuwenhuis & Albert Rubio (2001): Paramodulation-Based Theorem Proving. In: Alan Robinson & Andrei Voronkov: Handbook of Automated Reasoning, chapter 7 I. Elsevier, pp. 371–443, doi:10.1016/B978-044450813-3/50009-6.
  21. Christos H. Papadimitriou (1981): On the complexity of integer programming. Journal of the ACM 28(4), pp. 765–768, doi:10.1145/322276.322287.
  22. Juan Antonio Navarro Pérez & Andrei Voronkov (2008): Proof Systems for Effectively Propositional Logic. In: Alessandro Armando, Peter Baumgartner & Gilles Dowek: Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, LNCS 5195. Springer, pp. 426–440, doi:10.1023/A:1005806324129.
  23. Knot Pipatsrisawat & Adnan Darwiche (2009): On the Power of Clause-Learning SAT Solvers with Restarts. In: CP, Lecture Notes in Computer Science 5732. Springer, pp. 654–668, doi:10.1007/11591191_40.
  24. Ruzica Piskac, Leonardo Mendonça de Moura & Nikolaj Bjørner (2010): Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. Journal of Automated Reasoning 44(4), pp. 401–424, doi:10.1007/s10817-009-9161-6.
  25. David A. Plaisted (1984): Complete Problems in the First-Order Predicate Calculus. Journal of Computer and System Sciences 29, pp. 8–35, doi:10.1016/0022-0000(84)90010-2.
  26. João P. Marques Silva & Karem A. Sakallah (1996): GRASP - a new search algorithm for satisfiability. In: International Conference on Computer Aided Design, ICCAD. IEEE Computer Society Press, pp. 220–227, doi:10.1109/ICCAD.1996.569607.
  27. Fabian M. Suchanek, Gjergji Kasneci & Gerhard Weikum (2007): Yago: a core of semantic knowledge. In: Carey L. Williamson, Mary Ellen Zurko, Peter F. Patel-Schneider & Prashant J. Shenoy: Proceedings of the 16th International Conference on World Wide Web, WWW 2007, Banff, Alberta, Canada, May 8-12, 2007. ACM, pp. 697–706, doi:10.1145/1242572.1242667.
  28. Martin Suda, Christoph Weidenbach & Patrick Wischnewski (2010): On the Saturation of YAGO. In: Automated Reasoning, 5th International Joint Conference, IJCAR 2010, LNAI 6173. Springer, Edinburgh, United Kingdom, pp. 441–456, doi:10.1007/978-3-642-14203-1_38.
  29. Christoph Weidenbach (2017): Do Portfolio Solvers Harm?. In: Giles Reger & Dmitriy Traytel: ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017, EPiC Series in Computing 51. EasyChair, pp. 76–81, doi:10.29007/vpxm.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org