We consider instantiation-based theorem proving whereby instances of clauses are generated by certain inferences, and where inconsistency is detected by proposition tests. We give a model construction proof of completeness by which restrictive inference systems as well as admissible simplification techniques can be justified. Another contribution of the paper are inference systems that allow one to also employ decision procedures for first-order fragments more complex than propositional logic. The decision provides for an approximate consistency test, and the instance generation inference system is a means of successively refining the approximation.

Compares three approaches to polynomial-time decidability for uniform word problems for quasi-varieties. Two of the approaches, by T. Evans (1951) and S. Burris (1995), respectively, are semantic, referring to certain embeddability and axiomatizability properties. The third approach is more proof-theoretic in nature, inspired by D. McAllester's (1993) concept of local inference. We define two closely related notions of locality for equational Horn theories and show that both of the criteria of Evans and Burris lie in between these two concepts. In particular, the variant we call "stable locality" is shown to subsume both Evans' and Burris's methods.

No abstract available.

We define order locality to be a property of clauses relative to a term ordering. This property generalizes the subformula property for proofs where the terms appearing in proofs can be bounded, under the given ordering, by terms appearing in the goal clause. We show that when a clause set is order local, then the complexity of its ground entailment problem is a function of its structure (e.g., full versus Horn clauses), and the ordering used. We prove that, in many cases, order locality is equivalent to a clause set being saturated under ordered resolution. This provides a means of using standard resolution theorem provers for testing order locality and transforming non-local clause sets into local ones. We have used the Saturate system to automatically establish complexity bounds for a number of nontrival entailment problems relative to complexity classes which include polynomial and exponential time and co-NP.

We consider the restriction of the guarded fragment to the two-variable case where, in addition, binary relations may be specified as transitive. We show that (i) this very restricted form of the guarded fragment without equality is undecidable and that (ii) when allowing non-unary relations to occur only in guards, the logic becomes decidable. The latter subclass of the guarded fragments the one that occurs naturally when translating multi-modal logics of the type Kg/sub 4/ S/sub 4/ or S5 into first-order logic. We also show that the loosely guarded fragment without equality and with a single transitive relation is undecidable.

We give a new decision procedure for the guarded fragment with equality. The procedure is based on resolution with superposition. We argue that this method will be more useful in practice than methods based on the enumeration of certain finite structures. It is surprising to see that one does not need any sophisticated simplification and redundancy elimination method to make superposition terminate on the class of clauses that is obtained from the clausification of guarded formulas. Yet the decision procedure obtained is optimal with regard to time complexity. We also show that the method can be extended to the loosely guarded fragment with equality.

We propose inference systems for binary relations that satisfy composition laws such as transitivity. Our inference mechanisms are based on standard techniques from term rewriting and represent a refinement of chaining methods as they are used in the context of resolution-type theorem proving. We establish the refutational completeness of these calculi and prove that our methods are compatible with the usual simplification techniques employed in refutational theorem provers, such as subsumption or tautology deletion. Various optimizations of the basic chaining calculus will be discussed for theories with equality and for total orderings. A key to the practicality of chaining methods is the extent to which so-called variable chaining can be avoided. We demonstrate that rewrite techniques considerably restrict variable chaining and that further restrictions are possible if the transitive relation under consideration satisfies additional properties, such as symmetry. But we also show that variable chaining cannot be completely avoided in general.

We define order locality to be a property of clauses relative to a term ordering. This property is a kind of generalization of the subformula property for proofs where terms arising in proofs are bounded, under the given ordering, by terms appearing in the goal clause. We show that when a clause set is order local, then the complexity of its ground entailment problem is a function of its structure (e.g., full versus Horn clauses), and the ordering used. We prove that, in many cases, order locality is equivalent to a clause set being saturated under ordered resolution. This provides a means of using standard resolution theorem provers for testing order locality and transforming non-local clause sets into local ones. We have used the Saturate system to automatically establish complexity bounds for a number of nontrivial entailment problems relative to complexity classes which include polynomial and exponential time and co-NP.

We introduce a class of restrictions for the ordered paramodulation and superposition calculi (inspired by the basic strategy for narrowing), which forbid paramodulation inferences at terms introduced by substitutions from previous inference steps. In addition we introduce restrictions based on term selection rules and redex orderings, which are general criteria for delimiting the terms which are available for inferences. These refinements are compatible with standard ordering restrictions and are complete without paramodulation into variables or using functional reflexivity axioms. We prove refutational completeness in the context of deletion rules, such as simplification by rewriting (demodulation) and subsumption, and of techniques for eliminating redundant inferences.

We propose inference systems for dealing with transitive relations in the context of resolution-type theorem proving. These inference mechanisms are based on standard techniques from term rewriting and represent a refinement of chaining methods. We establish their refutational completeness and also prove their compatibility with the usual simplification techniques used in rewrite-based theorem provers. A key to the practicality of chaining techniques is the extent to which so-called variable chainings can be restricted. We demonstrate that rewrite techniques considerably restrict variable chaining, though we also show that they cannot be completely avoided for transitive relations in general. If the given relation satisfies additional properties, such as symmetry, further restrictions are possible. In particular, we discuss (partial) equivalence relations and congruence relations.>

We present various refutationally complete calculi for first-order clauses with equality that allow for arbitrary selection of negative atoms in clauses. Refutational completeness is established via the use of well-founded orderings on clauses for defining a Herbrand model for a consistent set of clauses. We also formulate an abstract notion of redundancy and show that the deletion of redundant clauses during the theorem proving process preserves refutational completeness. It is often possible to compute the closure of non-trivial sets of clauses under application of non-redundant inferences. The refutation of goals for such complete sets of clauses is simpler than for arbitrary sets of clauses, in particular it suffices to consider only those proofs that have support from the goals, without compromising refutational completeness. For certain classes of formulas the search space can be restricted even further, as we demonstrate for so-called quasi-Horn clauses. The results in this paper contain as special cases or generalize many known results about Knuth–Bendix-like completion procedures (for equations, Horn clauses, and Horn clauses with Boolean conditions), completion of first-order clauses by clausal rewriting, and inductive theorem proving for Horn clauses.

The authors investigate the relationship between set constraints and the monadic class of first-order formulas and show that set constraints are essentially equivalent to the monadic class. From this equivalence, they infer that the satisfiability problem for set constraints is complete for NEXPTIME. More precisely, it is proved that this problem has a lower bound of NTIME(c/sup n/log n/), for some c>0. The relationship between set constraints and the monadic class also gives decidability and complexity results for certain practically useful extensions of set constraints, in particular "negative" projections and subterm equality tests.>

Abstract This paper describes the design and implementation of the FOAM text formatting system. FOAM runs on an 8085 microprocessor system under CP/M and produces output on Diablo printers. The main feature of the system is that it supports two levels of formatting. On a meta level, the system accepts descriptions of text and document classes together with formatting styles for text components. From the description, a specific instance of a formatter is generated. This formatter, then, on the text level accepts the input of a text of the described class and produces a formatted document as specified by the formatting styles.

In this paper the problems of parameter passing and implementation for parameterized algebraic specifications are studied on a proof theoretic level.A syntactic equivalent to the semantic notion of persistency deemed by the ADJ group is introduced for parameterized specifications.It is shown to lead to similar results concerning the correctness of parameter passing and the nesting of parameters.Then a formal notion of implementation is developed for persistent specifications.It allows for developing implementations in a stepwise fashion.Moreover, implementations for instantiations (i.e., specifications that result from applying a parameterized specification to an actual parameter) can be constructed mechanically from given implementations for the specification procedure and the actual parameter.Correctness of implementation is required only with respect to observable properties of a specification, so an increased amount of optimization is allowed.