Abstract
There are syntactically identifiable situations in which reduction does not occur in chain format linear deduction systems, i.e. situations in which linear-input subdeductions are performed. Three methods of detecting these situations are described in this paper. The first method (Horn subset analysis) focuses on Horn input chains while the second (LISS analysis) and third (LISL analysis) are successive generalisations of the first method. A significant benefit that may be derived from detecting linear-input subdeductions is the applicability of a truth value deletion strategy in such subdeductions. The completeness of the deletion strategy is proved, and its efficacy indicated.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Andrews P.B., Resolution with Merging, In Journal of the ACM 15(3), ACM Press, New York, NY, (1968), 367–381.
Brown F.M., SLM, Internal Memo #72, Department of Artificial Intelligence, University of Edinburgh, Edinburgh, Scotland, (1974).
Bundy A., The Computer Modelling of Mathematical Reasoning, Academic Press, London, England, (1983).
Chang C-L., The Unit Proof and the Input Proof in Theorem Proving, In Journal of the ACM 17(4), ACM Press, New York, NY, (1970), 698–707.
Chang C-L., and Lee R.C-T., Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, NY, (1973).
Fleisig S., Loveland D.W., Smiley A.K., and Yarmush D.L., An Implementation of the Model Elimination Proof Procedure, In Journal of the ACM 21(1), ACM Press, New York, NY, (1974), 124–139.
Kowalski R., and Kuehner D., Linear Resolution with Selection Function, In Artificial Intellience 2, Elsevier Science, Amsterdam, The Netherlands, (1971), 227–260.
Loveland D.W., A Simplified Format for the Model Elimination Theorem-Proving Procedure, In Journal of the ACM 16(3), ACM Press, New York, NY, (1969), 349–363.
Loveland D.W., A Linear Format for Resolution, In Laudet M. et al. (Ed.), Proceedings of the IRIA Symposium on Automatic Demonstration (Versailles, France, 1968), Springer-Verlag, New York, NY, (1970), 147–162.
Luckham D., Refinement Theorems in Resolution Theory, In Laudet M. et al. (Ed.), Proceedings of the Symposium on Automatic Demonstration (Versailles, France, 1968), Springer-Verlag, New York, NY, (1970), 163–190.
McRobbie M.A., Meyer R.K., and Thistlewaite P.B., Towards Efficient “Knowledge-Based” Automated Theorem Proving for Non-Standard Logics, In Lusk E., Overbeek R. (Ed.), Proceedings of the 9th International Conference on Automated Deduction (Argonne, IL, 1988), (Goos G., Hartmanis J. (Ed.), Lecture Notes in Computer Science 310), Springer-Verlag, New York, NY, (1988), 197–217.
Meltzer B., Theorem-proving for computers: Some results on resolution and renaming, In The Computer Journal 8, The Britsh Computer Society, London, England, (1966), 341–343.
Minker J., and Zanon G., An Extension to Linear Resolution with Selection Function, In Information Processing Letters 14(4), Elsevier Science, Amsterdam, The Netherlands, (1982), 191–194.
Plaisted D.A., A Simplified Problem Reduction Format, In Artificial Intelligence 18, Elsevier Science, Amsterdam, The Netherlands, (1982), 227–261.
Reboh R., Raphael B., Yates R.A., Kling R.E., and Velarde C., Study of automatic theorem proving programs, Technical Note 72, Artificial Intelligence Center, SRI International, Menlo Park, CA, (1972).
Ringwood G.A., SLD: A Folk Acronym, In Moss C. (Ed.), Logic Programming Newsletter 2(1), Association for Logic Programming, London, England, (1988), 5–7.
Robinson J.A., Automatic Deduction with Hyper-resolution, In International Journal of Computer Mathematics 1, Gordon and Breach, London, England, (1965), 227–234.
Shostak R.E., Refutation Graphs, In Artificial Intelligence 7, Elsevier Science, Amsterdam, The Netherlands, (1976), 51–64.
Slagle J.R., Automatic Theorem Proving with Renamable and Semantic Resolution, In Journal of the ACM 14(4), ACM Press, New York, NY, (1967), 687–697.
Stickel M.E., A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler, In Siekmann J.H. (Ed.), Proceedings of the 8th International Conference on Automated Deduction (Oxford, England, 1986), (Goos G., Hartmanis J. (Ed.). Lecture Notes in Computer Science 230), Springer-Verlag, New York, NY, (1986), 573–587.
Sutcliffe G., Complete Linear Derivation Systems for General Clauses, In Wos L. (Ed.), Association for Automated Reasoning Newsletter (13), Association for Automated Reasoning, Argonne, Il, (1989), 3–4.
Sutcliffe G., A General Clause Theorem Prover, In Stickel M.E. (Ed.), Proceedings of the 10th International Conference on Automated Deduction (Kaiserslautern, Germany, 1990), (Siekmann J.H. (Ed.), Lecture Notes in Artificial Intelligence 449), Springer-Verlag, New York, NY, (1990), 675–676.
Sutcliffe G., The Semantically Guided Linear Deduction System, In Kapur, D. (Ed.), Proceedings of the 11th International Conference on Automated Deduction (Saratoga Springs, NY, 1992), Springer-Verlag, New York, NY, (1992).
Tarver M., An Examination of the Prolog Technology Theorem Prover, In Stickel M. (Ed.), Proceedings of the 10th International Conference on Automated Deduction (Kaiserslautern, Germany, 1990), (Siekmann J.H. (Ed.), Lecture Notes in Artificial Intelligence 449), Springer-Verlag, New York, NY, (1990), 322–335.
Wakayama T., and Payne T.H., Case-Free Programs: An Abstraction of Definite Horn Programs, In Stickel M. (Ed.), Proceedings of the 10th International Conference on Automated Deduction (Kaiserslautern, Germany, 1990), (Siekmann J.H. (Ed.), Lecture Notes in Artificial Intelligence 449), Springer-Verlag, New York, NY, (1990), 87–101.
Wos L., Automated Reasoning — 33 Basic Research Problems, Prentice-Hall, Englewood Cliffs, New Jersey, (1988).
Zamov N.K., and Sharonov V.I., On a class of strategies which can be used to prove theorems by the resolution principle, In (In Russian) (Ed.), Issled, po konstruktivnoye matematikye i matematicheskoie logikye III(16), National Lending Library Russian Translating Program 5857, Boston Spa, Yorkshire, (1969), 54–64.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sutcliffe, G. (1992). Linear-input subset analysis. In: Kapur, D. (eds) Automated Deduction—CADE-11. CADE 1992. Lecture Notes in Computer Science, vol 607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55602-8_171
Download citation
DOI: https://doi.org/10.1007/3-540-55602-8_171
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55602-2
Online ISBN: 978-3-540-47252-0
eBook Packages: Springer Book Archive