Non-resolution theorem proving
type: Item
instance of: scholarly article
title: Non-resolution theorem proving
zbMATH Open document ID: 0358.68131
DOI: 10.1016/0004-3702(77)90012-1
author: W. W. Bledsoe
published in: Artificial Intelligence
publication date: 1977-01-01T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 3559034
describes a project that uses: REDUCE
MaRDI profile type: Publication
full work available at URL: 0004-3702(77)90012-1
OpenAlex ID: W2023139438
cites work: Q5624685
cites work: Q4088305
cites work: Splitting and reduction heuristics in automatic theorem proving
cites work: Computer proofs of limit theorems
cites work: A man-machine theorem-proving system
cites work: Proving Theorems about LISP Functions
cites work: Q5679729
cites work: Q5681544
cites work: Q5616174
cites work: Q5721424
cites work: Untersuchungen über das logische Schliessen. I
cites work: Semi-Automated Mathematics
cites work: Applications of symbol manipulation in theoretical physics
cites work: Semantic Resolution for Horn Sets
cites work: Q5670164
cites work: A paradigm for reasoning by analogy
cites work: Notes on central groupoids
cites work: Q5581665
cites work: Specialization of the form of deduction in the precicate calculus with equality and function symbols. I
cites work: Q4766612
cites work: Q5583066
cites work: Q5519616
cites work: The semantics of induction and the possibility of complete systems of inductive inference
cites work: The \(Q^*\) algorithm - a search strategy for a deductive question-answering system
cites work: A Human Oriented Logic for Automatic Theorem-Proving
cites work: A relaxation approach to splitting in an automatic theorem prover
cites work: Plane geometry theorem proving using forward chaining
cites work: Q5529027
cites work: A New Class of Automated Theorem-Proving Algorithms
cites work: Q5678447
cites work: An improved proof procedure1
cites work: A Semantically Guided Deductive System for Automatic Theorem Proving
cites work: Q5624683
cites work: Q5590294
cites work: Breadth-first search: some surprising results
cites work: Automatic Theorem Proving With Renamable and Semantic Resolution
cites work: Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
cites work: Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets
cites work: Experiment with an automatic theorem-prover having partial ordering inference rules
cites work: Experiments with a heuristic theorem-proving program for predicate calculus with equality
cites work: Reasoning about programs
cites work: Q3667965
description: scientific article; zbMATH DE number 3559034