A Human Oriented Logic for Automatic Theorem-Proving

DOI10.1145/321850.321858MaRDI QIDQ4098673zbMATH OpenOpenAlexFDO

Authors 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

Pattern recognition, speech recognition (68T10)

Cited in

(17)

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4098673)