Abstract
This article is the twenty-fourth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find an appropriate theory for modulating across argument and across literal boundaries. Because demodulation has proved so useful—is most cases, even crucial—to automated reasoning, extending this concept to permit canonicalization to be applied at the predicate and at the clause and subclause levels merits exploration. For evaluating a proposed solution to this research problem, we suggest problems from mathematics, logic, program verification, database inquiry, and the world of puzzles.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
BoyerR., LuskE., McCuneW., OverbeekR., StickelM., and WosL., ‘Set theory in first-order logic: Clauses for Gödel's axioms’, J. Automated Reasoning 2, 287–327 (1986).
KnuthD., and BendixP., ‘Simple word problems in universal algebras’, pp. 263–297 in Computational Problems in Abstract Algebra, ed. J.Leech, Pergamon Press, New York (1970).
McCharenJ., OverbeekR., and WosL., ‘Complexity and related enhancements for automated theorem-proving programs’, Computers and Mathematics with Applications 2, 1–16 (1976).
WosL., RobinsonG., CarsonD., and ShallaL., ‘The concept of demodulation in theorem proving’, J. ACM 14, 698–709 (1967).
WosL., Automated Reasoning: 33 Basic Research Problems, Prentice-Hall, Englewood Cliffs, New Jersey (1988).
WosL., OverbeekR., LuskE., and BoyleJ., Automated Reasoning: Introduction and Applications, 2nd edn., McGraw-Hill, New York (1992).
Author information
Authors and Affiliations
Additional information
This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.
Rights and permissions
About this article
Cite this article
Wos, L. The problem of demodulating across argument and literal boundaries. Journal of Automated Reasoning 9, 407–408 (1992). https://doi.org/10.1007/BF00245299
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00245299