A posthumous contribution by Larry Wos: excerpts from an unpublished column
From MaRDI portal
Publication:2102925
DOI10.1007/S10817-022-09617-3OpenAlexW4210619513WikidataQ114264017 ScholiaQ114264017MaRDI QIDQ2102925FDOQ2102925
Authors: 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
Recommendations
puzzleset of supportfirst-order logic modulo arithmetichistory of automated reasoningreasoning by instantiation
Cites Work
- Theory and Applications of Satisfiability Testing
- Title not available (Why is that?)
- Simplify: a theorem prover for program checking
- Faster, higher, stronger: E 2.3
- Title not available (Why is that?)
- Simplification by Cooperating Decision Procedures
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Title not available (Why is that?)
- A Computing Procedure for Quantification Theory
- Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
- Rewriting
- Combining superposition, sorts and splitting
- A survey of satisfiability modulo theory
- Proof Systems for Effectively Propositional Logic
- Efficient E-Matching for SMT Solvers
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- Fast Decision Procedures Based on Congruence Closure
- Automated deduction -- CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27--30, 2019. Proceedings
- On First-Order Model-Based Reasoning
- Handbook of automated reasoning. In 2 vols
- Refutational theorem proving for hierarchic first-order theories
- Model-based theory combination
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
- 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 Proof Method for Quantification Theory: Its Justification and Realization
- Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
- Title not available (Why is that?)
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
- Politeness and combination methods for theories with bridging functions
- SCL clause learning from simple models
- Revisiting enumerative instantiation
- Solving open questions and other challenge problems using proof sketches
- Schubert's steamroller problem: Formulations and solutions
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Otter 2.0
- Generalized completeness for SOS resolution and its application to a new notion of relevance
- Title not available (Why is that?)
- Description logic, theory combination, and all that. Essays dedicated to Franz Baader on the occasion of his 60th birthday
- Implementing Superposition in iProver (System Description)
Cited In (3)
Uses Software
This page was built for publication: A posthumous contribution by Larry Wos: excerpts from an unpublished column
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2102925)
