Larry Wos: visions of automated reasoning
From MaRDI portal
Publication:2102922
Recommendations
Cites work
- A case study in automated theorem proving: Finding sages in combinatory logic
- A combinator-based superposition calculus for higher-order logic
- A complete proof of correctness of the Knuth-Bendix completion algorithm
- A Computing Procedure for Quantification Theory
- A Fascinating Country in the World of Computing
- A Machine-Oriented Logic Based on the Resolution Principle
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- A Wos Challenge Met
- An implementation of hyper-resolution
- An overview of automated reasoning and related fields
- Automatic Theorem Proving With Renamable and Semantic Resolution
- Beweisalgorithmen für die Prädikatenlogik
- Citius altius fortius: lessons learned from the theorem prover Waldmeister
- Conquering the Meredith single axiom
- Double-negation elimination in some propositional logics
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- Equational inference, canonical proofs, and proof orderings
- Faster, higher, stronger: E 2.3
- Finding proofs in Tarskian geometry
- Hilbert's twenty-fourth problem
- Hilbert's Twenty-Fourth Problem
- scientific article; zbMATH DE number 1670763 (Why is no real title available?)
- scientific article; zbMATH DE number 4016226 (Why is no real title available?)
- scientific article; zbMATH DE number 5147179 (Why is no real title available?)
- scientific article; zbMATH DE number 4049135 (Why is no real title available?)
- scientific article; zbMATH DE number 41806 (Why is no real title available?)
- scientific article; zbMATH DE number 50648 (Why is no real title available?)
- scientific article; zbMATH DE number 53302 (Why is no real title available?)
- scientific article; zbMATH DE number 1252517 (Why is no real title available?)
- scientific article; zbMATH DE number 599028 (Why is no real title available?)
- scientific article; zbMATH DE number 1037485 (Why is no real title available?)
- scientific article; zbMATH DE number 2024619 (Why is no real title available?)
- scientific article; zbMATH DE number 1552532 (Why is no real title available?)
- scientific article; zbMATH DE number 1865568 (Why is no real title available?)
- scientific article; zbMATH DE number 2100042 (Why is no real title available?)
- scientific article; zbMATH DE number 794244 (Why is no real title available?)
- scientific article; zbMATH DE number 1418280 (Why is no real title available?)
- scientific article; zbMATH DE number 3219316 (Why is no real title available?)
- scientific article; zbMATH DE number 3254919 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3349331 (Why is no real title available?)
- Implementing Superposition in iProver (System Description)
- Layered clause selection for theory reasoning (short paper)
- New results on rewrite-based satisfiability procedures
- On deciding satisfiability by theorem proving with speculative inferences
- On First-Order Model-Based Reasoning
- On the reconstruction of proofs in distributed theorem proving: A Modified Clause-Diffusion method
- OTTER and the Moufang identity problem
- OTTER proofs in Tarskian geometry
- Paramodulation-based theorem proving
- Performance of clause selection heuristics for saturation-based theorem proving
- Playing with AVATAR
- Problems and Experiments for and with Automated Theorem-Proving Programs
- Proof simplification and automated theorem proving
- Proofs from THE BOOK. Including illustrations by Karl H. Hofmann
- Proving refutational completeness of theorem-proving strategies
- Proving Theorems with the Modification Method
- Questions concerning possible shortest single axioms for the equivalential calculus: An application of automated theorem proving to infinite domains
- Restricted combinatory unification
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Searching for circles of pure proofs
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Semantically-guided goal-sensitive reasoning: model representation
- Semigroups, Antiautomorphisms, and Involutions: A Computer Solution to an Open Problem, I
- Short single axioms for Boolean algebra
- Shortest axiomatizations of implicational S4 and S5
- Solution of the Robbins problem
- Superposition as a decision procedure for timed automata
- Superposition for -free higher-order logic
- Superposition with lambdas
- The Concept of Demodulation in Theorem Proving
- The kernel strategy and its use for the study of combinatory logic
- Theorem-proving with resolution and superposition
- Towards a foundation of completion procedures as semidecision procedures
- Vanquishing the XCB question: The methodological discovery of the last shortest single axiom for the equivalential calculus
Cited in
(7)- Set of support, demodulation, paramodulation: a historical perspective
- A Wos Challenge Met
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- A tour of Franz Baader's contributions to knowledge representation and automated deduction
- scientific article; zbMATH DE number 53302 (Why is no real title available?)
- scientific article; zbMATH DE number 1252517 (Why is no real title available?)
- The legacy of a great researcher
This page was built for publication: Larry Wos: visions of automated reasoning
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2102922)
