A Human Oriented Logic for Automatic Theorem-Proving

DOI10.1145/321850.321858zbMath0332.68061OpenAlexW2075469844MaRDI QIDQ4098673

Arthur J. Nevins

Publication date: 1974

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/1721.1/5807

Mathematics Subject Classification ID

Related Items (17)

Solving propositional satisfiability problems ⋮ Combination problems for commutative/monoidal theories or how algebra can help in equational unification ⋮ Tautology testing with a generalized matrix reduction method ⋮ Unification properties of commutative theories: A categorical treatment ⋮ Non-monotonic logic. I ⋮ Unification in varieties of completely regular semigroups ⋮ Experiments with resolution-based theorem-proving algorithms ⋮ A simplified problem reduction format ⋮ Unification theory ⋮ Plane geometry theorem proving using forward chaining ⋮ A relaxation approach to splitting in an automatic theorem prover ⋮ Unification in commutative theories ⋮ Non-resolution theorem proving ⋮ A pragmatic approach to resolution-based theorem proving ⋮ Linear programs for constraint satisfaction problems ⋮ A man-machine theorem-proving system ⋮ \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations

This page was built for publication: A Human Oriented Logic for Automatic Theorem-Proving