A pragmatic approach to resolution-based theorem proving
From MaRDI portal
Publication:3877068
DOI10.1007/BF00982291zbMath0436.68059OpenAlexW2040884237MaRDI QIDQ3877068
Publication date: 1980
Published in: International Journal of Computer & Information Sciences (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00982291
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Cites Work
- Unnamed Item
- Unnamed Item
- Non-resolution theorem proving
- A man-machine theorem-proving system
- Computer proofs of limit theorems
- Solving problems by formula manipulation in logic and linear inequalities
- Experiment with an automatic theorem-prover having partial ordering inference rules
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Resolution, Refinements, and Search Strategies: A Comparative Study
- A Human Oriented Logic for Automatic Theorem-Proving
- Proving Theorems about LISP Functions
- Symbolic Testing and the DISSECT Symbolic Evaluation System
- Constructive Methods in Program Verification
- A language extension for expressing constraints on data access
- Symbolic Evaluation and the Analysis of Programs
- MRPPS?An interactive refutation proof procedure system for question-answering
- 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 Built-in Theories Including Equality, Partial Ordering, and Sets
This page was built for publication: A pragmatic approach to resolution-based theorem proving
