Skip Navigation

The Computer Journal 1975 18(1):49-54; doi:10.1093/comjnl/18.1.49
© 1975 by British Computer Society
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrow Search for citing articles in:
ISI Web of Science (3)
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Slagle, J. R.
Right arrow Articles by Norton, L. M.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

Automated theorem-proving for the theories of partial and total ordering

J. R. Slagle * and L. M. Norton §

Heuristics Laboratory, Division of Computer Research and Technology, National Institutes of Health, Department of Health, Education and Welfare, Bethesda, Maryland, USA

To make further progress, resolution principle programs need to make better inferences and to make them faster. Previous papers of the authors have presented a fairly general approach for taking some advantage of the structure of special theories, for example, the theories of equality, partial ordering and sets, and described experiments with a program base on this approach. The object of the approach is to replace some or all of the axioms of the given theory by (refutation) complete, valid, efficient (in time) inference rules.

In this paper, the approach is used to develop an improved procedure for ‘building in’ partial ordering and a procedure for total ordering. These results may be stated roughly as follows.

1. If the five (not all independent) partial ordering axioms for {=, ≤, <} are replaced by the irreflexivity rule ri and the transitivity rule rt (for <), by an expansion rule, and by an extension to hyper-resolution, then refutation completeness is preserved.

2. If only the connectivity axiom, {x < y {vee} y] ≤ x}, is retained from the five total ordering axioms for {=, ≤, <} and if the other four are replaced by ri, rt, and an antisymmetry rule, refutation completeness is preserved.

A program using total ordering inference rules is then described. Differences between the rules as presented in the theoretical development and as implemented in the program are noted. The paper concludes with a discussion of the program's successful performance on a large collection of problems taken from published papers.

Received April 1973.

* Computer Science Laboratory, Communications Sciences Division, Naval Research Laboratory, Washington, D.C. 20375, USA.

§ Data Management Branch, DCRT, NIH.

Heuristics Laboratory, Division of Computer Research and Technology, National Institutes of Health, Department of Health, Education and Welfare, Bethesda, Maryland 20014, USA


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.