1 - 7 of 7 articles
A Prolog technology theorem prover (PTTP) is an extension of Prolog that is complete for the full first-order predicate calculus. It differs from Prolog in its use of unification with the occurs check for soundness, the model-elimination reduction rule that is added to Prolog inferences to make...
We show that two Boolean terms which are unifiable have a most general unifier, which can be described using the terms themselves and a single unifier. Techniques for finding a single unifier are given.
We propose criteria that any rule for inferring negative information from disjunctive databases should satisfy, and examine existing rules from this viewpoint. We then present a new inference rule, the ‘disjunctive database rule’ (DDR), and compare it to the existing rules with respect to the...
A new reduction rule is introduced for the connection graph proof procedure proposed by Kowalski in 1975. The new rule considers sets of values which clause variables may take. Application of the rule often leads to massive removals of links. A proof system in which the new rule is included has...
We construct equivalent “localized” versions of a formula, adding assumptions simultaneously to various locations, where the particular location determines what is added. Inference rules that take advantage of localized formulas are presented for sequent calculi in which the left hand side of...
This article is the eighth of a series of articles discussing various open research problems in automated reasoning. Here we focus on self-analysis and the weighting strategy. The problem proposed for research asks one to find a means for an automated reasoning program to self-analytically...
This note reports about the implementation of AC-unification algorithms, based on the variable-abstraction method of Stickel and on the constant-abstraction method of Livesey, Siekmann, and Herold. We give a set of 105 benchmark examples and compare execution times for implementations of the two...
Read and print from thousands of top scholarly journals.
Continue with Facebook
Log in with Microsoft
Already have an account? Log in
Bookmark this article. You can see your Bookmarks on your DeepDyve Library.
To save an article, log in first, or sign up for a DeepDyve account if you don’t already have one.
Sign Up Log In
To subscribe to email alerts, please log in first, or sign up for a DeepDyve account if you don’t already have one.
To get new article updates from a journal on your personalized homepage, please log in first, or sign up for a DeepDyve account if you don’t already have one.