A posthumous contribution by Larry Wos: excerpts from an unpublished column
From MaRDI portal
Publication:2102925
DOI10.1007/s10817-022-09617-3OpenAlexW4210619513WikidataQ114264017 ScholiaQ114264017MaRDI QIDQ2102925
Sophie Tourret, Christoph Weidenbach
Publication date: 12 December 2022
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-022-09617-3
puzzleset of supportfirst-order logic modulo arithmetichistory of automated reasoningreasoning by instantiation
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Schubert's steamroller problem: Formulations and solutions
- Refutational theorem proving for hierarchic first-order theories
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
- Generalized completeness for SOS resolution and its application to a new notion of relevance
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
- Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
- Description logic, theory combination, and all that. Essays dedicated to Franz Baader on the occasion of his 60th birthday
- Automated deduction -- CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27--30, 2019. Proceedings
- Politeness and combination methods for theories with bridging functions
- SCL clause learning from simple models
- Faster, higher, stronger: E 2.3
- Revisiting enumerative instantiation
- Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
- A Survey of Satisfiability Modulo Theory
- Model-based Theory Combination
- On First-Order Model-Based Reasoning
- A Proof Method for Quantification Theory: Its Justification and Realization
- Solving SAT and SAT Modulo Theories
- Proof Systems for Effectively Propositional Logic
- Simplify: a theorem prover for program checking
- Efficient E-Matching for SMT Solvers
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Fast Decision Procedures Based on Congruence Closure
- Simplification by Cooperating Decision Procedures
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Implementing Superposition in iProver (System Description)
- Theory and Applications of Satisfiability Testing
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- A Computing Procedure for Quantification Theory
- Solving open questions and other challenge problems using proof sketches
This page was built for publication: A posthumous contribution by Larry Wos: excerpts from an unpublished column
