A Human Oriented Logic for Automatic Theorem-Proving
From MaRDI portal
Publication:4098673
DOI10.1145/321850.321858zbMath0332.68061MaRDI QIDQ4098673
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
68T10: Pattern recognition, speech recognition
Related Items
Unification in commutative theories, 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