A Human Oriented Logic for Automatic Theorem-Proving
From MaRDI portal
Publication:4098673
DOI10.1145/321850.321858zbMath0332.68061OpenAlexW2075469844MaRDI 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
Related Items
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