Larry Wos: visions of automated reasoning
From MaRDI portal
Publication:2102922
DOI10.1007/s10817-022-09620-8OpenAlexW4214565566WikidataQ114264016 ScholiaQ114264016MaRDI QIDQ2102922
Michael J. Beeson, Maria Paola Bonacina, Geoff Sutcliffe, Michael K. Kinyon
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-09620-8
Related Items (1)
Uses Software
Cites Work
- Semantically-guided goal-sensitive reasoning: model representation
- On deciding satisfiability by theorem proving with speculative inferences
- Towards a foundation of completion procedures as semidecision procedures
- Theorem-proving with resolution and superposition
- Double-negation elimination in some propositional logics
- A case study in automated theorem proving: Finding sages in combinatory logic
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- Questions concerning possible shortest single axioms for the equivalential calculus: An application of automated theorem proving to infinite domains
- An implementation of hyper-resolution
- The kernel strategy and its use for the study of combinatory logic
- Solution of the Robbins problem
- Shortest axiomatizations of implicational S4 and S5
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Superposition for \(\lambda\)-free higher-order logic
- OTTER and the Moufang identity problem
- An overview of automated reasoning and related fields
- Short single axioms for Boolean algebra
- Hilbert's twenty-fourth problem
- Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus
- Searching for circles of pure proofs
- Superposition as a decision procedure for timed automata
- A combinator-based superposition calculus for higher-order logic
- Layered clause selection for theory reasoning (short paper)
- A Wos Challenge Met
- Restricted combinatory unification
- Faster, higher, stronger: E 2.3
- Finding proofs in Tarskian geometry
- On the reconstruction of proofs in distributed theorem proving: A Modified Clause-Diffusion method
- Beweisalgorithmen für die Prädikatenlogik
- Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
- On First-Order Model-Based Reasoning
- OTTER Proofs in Tarskian Geometry
- Playing with AVATAR
- Semigroups, Antiautomorphisms, and Involutions: A Computer Solution to an Open Problem, I
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Problems and Experiments for and with Automated Theorem-Proving Programs
- Proving Theorems with the Modification Method
- Equational inference, canonical proofs, and proof orderings
- Proving refutational completeness of theorem-proving strategies
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Hilbert's Twenty-Fourth Problem
- Proofs from THE BOOK
- Citius altius fortius
- Implementing Superposition in iProver (System Description)
- Proof simplification and automated theorem proving
- New results on rewrite-based satisfiability procedures
- A Fascinating Country in the World of Computing
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- A Machine-Oriented Logic Based on the Resolution Principle
- Automatic Theorem Proving With Renamable and Semantic Resolution
- The Concept of Demodulation in Theorem Proving
- A Computing Procedure for Quantification Theory
- Superposition with lambdas
- Conquering the Meredith single axiom
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Larry Wos: visions of automated reasoning
