Completeness results for inequality provers

DOI10.1016/0004-3702(85)90015-3zbMath0598.68059OpenAlexW2058156127MaRDI QIDQ1079960

B. George

Publication date: 1985

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0004-3702(85)90015-3

zbMATH Keywords

resolutioncompleteness theoremautomated deductionfactoringelementary calculusordering of the real numbersproofs of propositions about dense total orders without endpointsrule of chainingself-chaining

Mathematics Subject Classification ID

Total orders (06A05) Software, source code, etc. for problems pertaining to ordered structures (06-04)

Related Items (4)

Completeness results for inequality provers ⋮ Theorem proving in cancellative abelian monoids (extended abstract) ⋮ The problem of reasoning from inequalities ⋮ Ordered chaining for total orderings

Cites Work

• Completeness results for inequality provers
• Mechanical Theorem-Proving by Model Elimination
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Completeness results for inequality provers