A Human Oriented Logic for Automatic Theorem-Proving
From MaRDI portal
Publication:4098673
DOI10.1145/321850.321858zbMATH Open0332.68061OpenAlexW2075469844MaRDI QIDQ4098673FDOQ4098673
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
Cited In (17)
- Unification theory
- Linear programs for constraint satisfaction problems
- Unification properties of commutative theories: A categorical treatment
- Unification in commutative theories
- A pragmatic approach to resolution-based theorem proving
- Solving propositional satisfiability problems
- Plane geometry theorem proving using forward chaining
- Non-resolution theorem proving
- A man-machine theorem-proving system
- \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations
- Non-monotonic logic. I
- Experiments with resolution-based theorem-proving algorithms
- Combination problems for commutative/monoidal theories or how algebra can help in equational unification
- A simplified problem reduction format
- Tautology testing with a generalized matrix reduction method
- A relaxation approach to splitting in an automatic theorem prover
- Unification in varieties of completely regular semigroups
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)
