One formulation of the concept of logic programming is the notion of an abstract logic programming language. Central to its definition is a uniform proof, which enforces the requirements of inference direction, including goal-directedness, and the duality of readings, both declarative and procedural. We use this technology to investigate disjunctive logic programming (DLP), an extension of traditional logic programming that permits disjunctive program clauses. This extension has been considered by some to be inappropriately identified with logic programming because the indefinite reasoning introduced by disjunction violates the goal-oriented search directionality that is central to logic programming. We overcome this criticism by showing that the requirement of uniform provability can be realized in a logic which is more general than that of DLP under a modest, sound modification of programs. We use this observation to derive inference rules that capture the essential proof structure of InH-Prolog (Inheritance Near-Horn Prolog), a known proof procedure for DLP.

Logic can be defined as the formal study of reasoning; if we replace “formal” by “mechanical” we can place almost the entire set of methodologies used in the field of automated theorem proving (ATP) within the scope of logic. Because of the goals of ATP, if not always the methodologies, ATP has been considered to be within the domain of AI. We explore the methodologies of ATP, including the logics that underlie the theorem provers, and discuss some of the mechanisms that utilize these logics. These include term rewriting systems, mathematical induction, inductionless induction and even mixed integer programming. The ATP field, via resolution, has even provided the foundation for an exciting AI and database programming language, PROLOG. We conclude with a new method for extending the PROLOG system to work with non-Horn clause sets within a positive logic format, particularly simple for “slightly non-Horn” clause sets.

Although the classical problem reducUon format for orgamzmg automauc proof search is incomplete, a complete extension of the format is known ElimmaUon of tdentlcal descendent subgoals is a well-known deletion rule for the classical format but is not obviously vahd m the extended format.Because of ~ts mtumve appeal and ease of apphcatlon, one would wish to know that the rule ~s safe to use m the extended format It ts shown here that the deleuon rule is indeed safe The result appears to be decidedly nontnvml

This paper concerns both the complexity aspects of PA and the pragmatics of improving algorithms for dealing with restricted subcases of PA for uses such as program verification. We improve the Cooper-Presburger decision procedure and show that the improved version permits us to obtain time and space upper bounds for PA classes restricted to a bounded number of alternations of quantifiers. The improvement is one exponent less than the upper bounds for the decision problem for full PA. The pragmatists not interested in complexity bounds can read the results as substantiation of the intuitive feeling that the improvement to the Cooper-Presburger algorithm is a real, rather than ineffectual, improvement. (It can be easily shown that the bounds obtained here are not achievable using the Cooper-Presburger procedure).

The representation power of goal-subgoal trees and the adequacy of this form of problem reduction is considered. A number of inadequacies in the classical form are illustrated, and two versions of a syntactic procedure incorporating extensions are given. Although the form of the corrections are suggested from resolution theory results, and the value of this connection emphasized, the paper discusses the goal tree format and its extensions on an informal level.

The model elimination (ME) and resolution algorithms for mechanical theorem-proving were implemented so as to maximize shared features. The identical data structures and large amount of common programming permit meaningful comparisons when the two programs are run on standard problems. ME does better on some classes of problems, and resolution better on others. The depth-first search strategy used in this ME implementation affects the performance profoundly. Other novel features in the implementation are new control parameters to govern extensions, and modified rules for generating and rejecting chains. The resolution program incorporates unit preference and set-of-support. An appendix reproduces the steps of a machine-derived ME refutation.

The linked conjunct, resolution, matrix reduction, and model elimination proof procedures constitute a nearly exhaustive list of the basic Herbrand proof procedures introduced in the 1960's.Each was introduced as a hopefully efficient complete procedure for the first order predicate calculus for the purpose of mechanical theorem proving.This paper contains a demonstration that versions of these procedures can be highly related in their design.S-linear resolution, a particular strategy of resolution previously proposed, is seen to possess a natural refinement isomorphic at ground level to a refinement of the model elimination procedure.There is also an isomorphism at the general level between a less natural s-linear resolution refinement and the model elimination refinement.The model elimination procedure is also interpreted within the linked conjunct and matrix reduction procedures.An alternate interpretation of these results is that, very roughly, the procedures other than resolution can be viewed as forms of linear resolution.

Brief consideration is given to some properties of three measures of complexity based on the length of minimal descriptive programs. Although the measures explicitly deal with finite sequences, the complexity of an infinite sequence can be regarded as a function mapping each positive integer n to the complexity of the initial segment of length n. Some properties of a complexity hierarchy of infinite sequences with respect to one of the measures is considered.

article Free AccessA Simplified Format for the Model Elimination Theorem-Proving Procedure Author: D. W. Loveland Carnegie-Mellon University, Pittsburgh, Pennsylvania Carnegie-Mellon University, Pittsburgh, PennsylvaniaView Profile Authors Info & Claims Journal of the ACMVolume 16Issue 3pp 349–363https://doi.org/10.1145/321526.321527Published:01 July 1969Publication History 112citation494DownloadsMetricsTotal Citations112Total Downloads494Last 12 Months26Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

No abstract available.

A proof procedure based on a theorem of Herbrand and utilizing the matching technique of Prawitz is presented. In general, Herbrand-type proof procedures proceed by generating over increasing numbers of candidates for the truth-functionally contradictory statement the procedures seek. A trial is successful when some candidate is in fact a contradictory statement. In procedures to date the number of candidates developed before a contradictory statement is found (if one is found) varies roughly exponentially with the size of the contradictory statement. (“Size” might be measured by the number of clauses in the conjunctive normal form of the contradictory statement.) Although basically subject to the same rate of growth, the procedure introduced here attempts to drastically trim the number of candidates at an intermediate level of development. This is done by retaining beyond a certain level only candidates already “partially contradictory.” The major task usually is finding the partially contradictory sets. However, the number of candidate sets required to find these subsets of the contradictory set is generally much smaller than the number required to find the full contradictory set.