A posthumous contribution by Larry Wos: excerpts from an unpublished column
type: Item
instance of: scholarly article
title: A posthumous contribution by Larry Wos: excerpts from an unpublished column
author: Sophie Tourret
author: Christoph Weidenbach
published in: Journal of Automated Reasoning
publication date: 2022-12-12T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7632085
zbMATH Keywords: history of automated reasoning
zbMATH Keywords: reasoning by instantiation
zbMATH Keywords: set of support
zbMATH Keywords: puzzle
zbMATH Keywords: first-order logic modulo arithmetic
describes a project that uses: iProver
describes a project that uses: VAMPIRE
describes a project that uses: SPASS
describes a project that uses: CVC4
describes a project that uses: OTTER
describes a project that uses: z3
describes a project that uses: MiniSat
describes a project that uses: TPTP
describes a project that uses: SIMPLIFY
MaRDI profile type: Publication
full work available at URL: s10817-022-09617-3
OpenAlex ID: W4210619513
Wikidata QID: Q114264017
cites work: Rewrite-based Equational Theorem Proving with Selection and Simplification
cites work: Refutational theorem proving for hierarchic first-order theories
cites work: Q5503674
cites work: Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
cites work: Q4989394
cites work: On First-Order Model-Based Reasoning
cites work: Description logic, theory combination, and all that. Essays dedicated to Franz Baader on the occasion of his 60th birthday
cites work: Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
cites work: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
cites work: Politeness and combination methods for theories with bridging functions
cites work: A Computing Procedure for Quantification Theory
cites work: Rewriting
cites work: Simplify: a theorem prover for program checking
cites work: Efficient E-Matching for SMT Solvers
cites work: Model-based theory combination
cites work: Q2479551
cites work: Implementing Superposition in iProver (System Description)
cites work: Theory and Applications of Satisfiability Testing
cites work: SCL clause learning from simple models
cites work: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
cites work: A Proof Method for Quantification Theory: Its Justification and Realization
cites work: Generalized completeness for SOS resolution and its application to a new notion of relevance
cites work: Q5581665
cites work: A Survey of Satisfiability Modulo Theory
cites work: Simplification by Cooperating Decision Procedures
cites work: Fast Decision Procedures Based on Congruence Closure
cites work: Solving SAT and SAT Modulo Theories
cites work: Proof Systems for Effectively Propositional Logic
cites work: Revisiting enumerative instantiation
cites work: Q3150300
cites work: Handbook of automated reasoning. In 2 vols
cites work: Faster, higher, stronger: E 2.3
cites work: Schubert's steamroller problem: Formulations and solutions
cites work: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
cites work: Automated deduction -- CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27--30, 2019. Proceedings
cites work: Using hints to increase the effectiveness of an automated reasoning program: Case studies
cites work: Solving open questions and other challenge problems using proof sketches
cites work: Combining superposition, sorts and splitting
cites work: Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
cites work: Q5507984
cites work: Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
cites work: Otter 2.0
DOI: 10.1007/S10817-022-09617-3
description: scientific article; zbMATH DE number 7632085