Larry Wos: visions of automated reasoning
type: Item
instance of: scholarly article
title: Larry Wos: visions of automated reasoning
author: Michael Beeson
author: Maria Paola Bonacina
author: Geoff Sutcliffe
author: Michael K. Kinyon
published in: Journal of Automated Reasoning
publication date: 2022-12-12T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7632080
zbMATH Keywords: Larry Wos
zbMATH Keywords: automated reasoning
Wikidata QID: Q114264016
describes a project that uses: EQP
describes a project that uses: iProver
describes a project that uses: Prover9
describes a project that uses: AURA
describes a project that uses: VAMPIRE
describes a project that uses: SPASS
describes a project that uses: Waldmeister
describes a project that uses: OTTER
MaRDI profile type: Publication
full work available at URL: s10817-022-09620-8
OpenAlex ID: W4214565566
cites work: Proofs from THE BOOK
cites work: New results on rewrite-based satisfiability procedures
cites work: Q4000281
cites work: Equational inference, canonical proofs, and proof orderings
cites work: Rewrite-based Equational Theorem Proving with Selection and Simplification
cites work: Q4524792
cites work: Double-negation elimination in some propositional logics
cites work: OTTER Proofs in Tarskian Geometry
cites work: Finding proofs in Tarskian geometry
cites work: Superposition for \(\lambda\)-free higher-order logic
cites work: Superposition with lambdas
cites work: Restricted combinatory unification
cites work: A combinator-based superposition calculus for higher-order logic
cites work: On the reconstruction of proofs in distributed theorem proving: A Modified Clause-Diffusion method
cites work: Q4941840
cites work: On First-Order Model-Based Reasoning
cites work: Q4847004
cites work: Towards a foundation of completion procedures as semidecision procedures
cites work: On deciding satisfiability by theorem proving with speculative inferences
cites work: Semantically-guided goal-sensitive reasoning: model representation
cites work: Semantically-guided goal-sensitive reasoning: inference system and completeness
cites work: Proving Theorems with the Modification Method
cites work: A Computing Procedure for Quantification Theory
cites work: Implementing Superposition in iProver (System Description)
cites work: Shortest axiomatizations of implicational S4 and S5
cites work: Superposition as a decision procedure for timed automata
cites work: Q4816538
cites work: Layered clause selection for theory reasoning (short paper)
cites work: Citius altius fortius
cites work: Q3786024
cites work: Q3028369
cites work: Proving refutational completeness of theorem-proving strategies
cites work: A complete proof of correctness of the Knuth-Bendix completion algorithm
cites work: Proof simplification and automated theorem proving
cites work: Q5581665
cites work: Problems and Experiments for and with Automated Theorem-Proving Programs
cites work: Solution of the Robbins problem
cites work: Short single axioms for Boolean algebra
cites work: A case study in automated theorem proving: Finding sages in combinatory logic
cites work: Paramodulation-based theorem proving
cites work: An implementation of hyper-resolution
cites work: A Technique for Establishing Completeness Results in Theorem Proving with Equality
cites work: Q4345253
cites work: Playing with AVATAR
cites work: Q5624683
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q5541351
cites work: Theorem-proving with resolution and superposition
cites work: Faster, higher, stronger: E 2.3
cites work: Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
cites work: Automatic Theorem Proving With Renamable and Semantic Resolution
cites work: Q4003525
cites work: Hilbert's Twenty-Fourth Problem
cites work: Hilbert's twenty-fourth problem
cites work: Beweisalgorithmen für die Prädikatenlogik

Larry Wos: visions of automated reasoning (cites work)
cites work: Q4229404

Larry Wos: visions of automated reasoning (cites work)
cites work: A Wos Challenge Met

Larry Wos: visions of automated reasoning (cites work)
cites work: Semigroups, Antiautomorphisms, and Involutions: A Computer Solution to an Open Problem, I

Larry Wos: visions of automated reasoning (cites work)
cites work: Q3994754

Larry Wos: visions of automated reasoning (cites work)
cites work: The kernel strategy and its use for the study of combinatory logic

Larry Wos: visions of automated reasoning (cites work)
cites work: Searching for circles of pure proofs

Larry Wos: visions of automated reasoning (cites work)
cites work: OTTER and the Moufang identity problem

Larry Wos: visions of automated reasoning (cites work)
cites work: Conquering the Meredith single axiom

Larry Wos: visions of automated reasoning (cites work)
cites work: Q5507984

Larry Wos: visions of automated reasoning (cites work)
cites work: Q2754067

Larry Wos: visions of automated reasoning (cites work)
cites work: Q4297316

Larry Wos: visions of automated reasoning (cites work)
cites work: An overview of automated reasoning and related fields

Larry Wos: visions of automated reasoning (cites work)
cites work: A Fascinating Country in the World of Computing

Larry Wos: visions of automated reasoning (cites work)
cites work: Q4792019

Larry Wos: visions of automated reasoning (cites work)
cites work: Efficiency and Completeness of the Set of Support Strategy in Theorem Proving

Larry Wos: visions of automated reasoning (cites work)
cites work: The Concept of Demodulation in Theorem Proving

Larry Wos: visions of automated reasoning (cites work)
cites work: Q4443194

Larry Wos: visions of automated reasoning (cites work)
cites work: Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus

Larry Wos: visions of automated reasoning (cites work)
cites work: Q3433180

Larry Wos: visions of automated reasoning (cites work)
cites work: Questions concerning possible shortest single axioms for the equivalential calculus: An application of automated theorem proving to infinite domains

Larry Wos: visions of automated reasoning (DOI)
DOI: 10.1007/S10817-022-09620-8