Automated Reasoning in Higher Order Logic
This page was created and is maintained by Chad E Brown.
TPS & Simply Typed lambda-Calculus
Knowledge Based Theorem Proving
Map/Relation Algebra Reasoning
Decidable Fragments of Set Theory
Solving Set Variable Constraints
This article is reprented in the Festschrift for Peter B. Andrews
Church defines the syntax of simple type theory (taking negation, conjunction, and pi as primitive), abbreviations (including those for "natural numbers" [as Church numerals] from each type alpha), the rules of deduction (lambda conversion, substitution, modus ponens, and generalization), and the axioms (the expected logical axioms plus axioms giving infinity, descriptions, extensionality, and choice). He proves the deduction theorem and then examines the Peano axioms for naturals for each type a (such naturals are actually of type a'=aa(aa), as opposed to Andrew's representation at type o(oa)). These hold for i, i', i'', etc., but the successor need not be one to one for other types. He then shows how to make primitive recursive definitions for such types (the prototype example being the predecessor function). Primitive recursion involves a pairing operation on numerals (giving, of course, a higher type) and an interplay between numerals of different types (which have a correspondence given by a "translation" operator T [which uses the description operator and takes type a' to type a''] proven in the paper).
This article is reprented in the Festschrift for Peter B. Andrews
Andrews introduces three systems: T, which is essentially Church's system of type theory with only axioms 1-6; G, which is a formulation eliminating the cut-rule (he proves G is equivalent to T by using Smullyan's Unifying Principle of Abstract Consistency); and a resolution-style refutation system R. Cut-elimination for Schutte's [Schutte 1960] formulation of type theory [presumably a relational type theory] was first proven by Takahashi [Takahashi 1967].
He gives a proof that all wff's have a unique (up to alpha-beta) lambda-normal (i.e., beta-reduced) form by induction on the complexity of types involved in beta-redex's. Then, he associates wff's A with their lambda-normal form eta-A (where variables are chosen in a methodical way to ensure uniqueness). Abstract Consistency is modified for the higher-order setting by requiring of the class that if S union {A} is in the class then S union {eta-A} is in the class (and we treat forall as the pi operator). A semivaluation assigns a truth value to some wff's in a way which respects lambda-conversion, logical connectives, and quantifiers. Given any member S of an abstract consistency class, there is a semivaluation for which all members of S map to t (proven by a standard extension argument).
For every semivaluation V, the set {A | VA=t} is consistent. This is proven by constructing a "general model" where the domains are V-complexes--i.e., pairs of eta-wff's and values "agreeing" with the semivaluation V. This provides a notion of general model appropriate for T (elementary type theory).
It follows that every "abstract consistent" set is consistent.
Then, what can be considered the main results of the paper, the cut-elimination theorem for elementary type theory is proven. System G is introduced. The axioms are excluded middle for each atomic wff. The rules of inference are alpha conversion, beta expansion, rearrangement of disjunction components, weakening, negation introduction, conjunction introduction, existential generalization and universal generalization. (So, the idea is that we start from simple tautologies and "build" the theorem by introduction-style rules.) It follows easily that every theorem of G is a theorem of T. The converse implies cut-elimination (since G is cut-free). In order to prove the converse, preliminary lemmas giving beta-reduction, elimination-style rules and simplification as derived rules are proven. These results are used to prove that the class of finite sets of wff's {A1,...,An} for which G does not prove "-A1 or . . . or -An" is an abstract consistency class. Then, if T proves A, then -A has no model, so {-A} is not in the abstract consistency class above, and so G proves --A, thus G proves A. This proof relies on a semantic argument using Smullyan's Unifying Principle.
The final system, system R, is a resolution-style refutation system for sets of sentences based on alpha-conversion, beta-reduction, rearrangement of disjunctive components, simplification, negation and conjunctive elimination, existential instantiation (using a choice function ["existential parameter"] at each type to create Skolem terms), universal instantiation, substitution and cut. He proves that if a sentence is refutable in T, then it is refutable in R, by using Smullyan's Unifying Principle applied to the class of sets of wff's which are not refutable in R (after variables are replaced by new constants). [Note: in Andrews 1974, a new refutation system B is introduced which introduces new parameters to perform existential instantiation instead of using choice functions as system R does. The difference between the systems is that the negation of the axiom of choice can be refuted in R, but not in B. A wff is provable in T iff it is refutable in B. So, system R is stronger than B, and hence T.]
Systems G and R are, in some sense, dual. System G starts from simple tautologies (excluded middle for atomic wffs) and builds the theorem using "expansion/introduction/generalization" rules. System R starts from a formula to refute and derives a contradiction using "reduction/elimination/instantiation/substitution/cut" rules. System T is a Hilbert-style system (in the sense that we axiomatize propositional logic using a few tautologies and derive the rest from these using modus ponens).
The results and proofs in this paper concerning systems G and R are analogous to the results for first-order systems proven in Andrews 1986, Chapter 3.
The search for refutations in R is compared and contrasted to the search for resolution refutations in first-order logic. The most obvious differences are beta-reduction and the fact that substitution may introduce new logical constants, so that the application of rules which reduce the problem to a set of clauses cannot be solely a preprocessing step.
Finally, the author gives examples of refutations in R including a proof that the successor of a natural is a natural (taking successor and zero as primitive constants and "naturals" defined in terms of these) and the fixed-point theorem example (if an iterate of f has a unique fixed point, then f has a fixed point--he uses derived equality rules for reflexivity and replacement for this proof).
The author introduces a refutation system B in which a formula is refutable in B iff it is refutable in T. The system R of the 1971 paper is too strong since the axiom of choice can be refuted in R. The essential difference between B and R is that B uses a method akin to Rule C to handle existential quantifier elimination where R used Skolems (as a choice function).
He uses this system to show that statements of the form exists x1,...,xn A=B are provable in T iff there exists a substitution q for x1,...,xn such that q*A = q*B (where q*X means "apply q, then put the result into l-normal form, then rename variables in the standard 'h' way"). This implies that statements of the form A=B are decidable (they are provable iff they lambda contract to the same form up to alpha conversion), but statements of the form exists x1,...,xn A=B with n>0 are not decidable (as a consequence of the undecidability of unification).
Also, he shows that if C is a quantifier free formula, then forall x1,...,xn C is provable iff hC (lambda-contract and standardize bound variable names) is a (propositional) tautology.
He shows the undecidability of provability for the classes {exists z[A=B]} and {exists zC: C is quantifier free} directly by reducing them to the Post Correspondence Problem.
This paper concerns refuting a set of first-order clauses by finding acceptable matings of a set of occurrences of (some of) the clauses. The author begins by describing how a mating can be lifted from a simple (resolution) deduction (a deduction is made simple by requiring that each occurrence of a clause except the last is used exactly once to create a later resolvent). Such a mating is acceptable if every literal has a mate and every cycle contains a merge. A resolution refutation induces an acceptable mating. Furthermore, he proves that a set of clauses S has no model iff there is a set of occurrences T of clauses selected from S and an acceptable mating of the literal occurrences in T. Thus, an exhaustive search for such a mating is a complete refutation procedure. He outlines such a search procedure.
This paper describes how proof-*matings of first-order formulae can be used to construct natural deduction proofs of the formulae. The method uses plans which include the formula to be proven (with definitions instantiated), instructions for replicating quantifiers, a mating, and a substitution associated with the mating. Such a plan is associated with each "planned" line of a proof outline (natural deduction proof in which some lines are planned rather than justified). In such a proof outline, some lines are active and are sponsored by certain planned lines. The plan associated with the planned line contains information as to how to prove the planned line from the active lines it sponsors. Transformation rules are used to fill in the proof outline. Deducing rules take active lines to inferred new active lines (which take on as sponsors, the sponsors of their predecessor). Planning rules justify previous planned lines via newly created planned rules (with associated plans). These rules describe how to create a new plan associated with planned lines (using information about the ancestors of quantifiers and atoms) to reflect the new proof outline. While this paper only concerns first-order proofs, this method is apparently extended later to apply to type theoretical proofs.
This paper extends the notion of matings to formulas which are not in conjunctive normal form, thus releasing us from the bondage of clauses. The matrix representation of literals of a formula in nnf is introduced, and certain logical notions are defined. A c-instance is a ground instance of a universal formula with (possible) quantifier duplication. He shows a universal nns (negation-normal sentence) has no model iff it has a c-instance which is t-f contradictory (that is, any assignment of {t,f} to the literals assigns the sentence to f). He defines an amplification of a universal nns by quantifier duplication, normalization of bound variable names, and deletion of quantifiers. He defines a mating to be a binary relation on literal occurrences such that there is an associated substitution which makes all mated literals complementary. A refutation mating is one in which all truth-value assignments to literals under the condition that mated literals receive opposite values assign the formula to f. A p-acceptable mating is one in which all vertical paths contain mated literals. He shows that a quantifier-free nnf G has a substitution q such that qG is t-f contradictory iff G has a p-acceptable mating iff G has a refutation mating. (This does not imply every refutation mating is p-acceptable, or that every mating with substitution q which makes qG t-f contradictory is a refutation mating.) The key completeness result follows, that a universal nns D of first-order logic has no model iff some amplification of D has a refutation [p-acceptable] mating.
He outlines a refutation procedure which attempts to build a p-acceptable mating, backtracking when necessary, and duplicating quantifiers when no mating can be found with the current amplification. He also discusses refinements of the procedure and heuristics which can be added to the procedure. He proves that only outermost quantifiers need be duplicated to retain completeness, but such a restriction will introduce inefficiencies in some cases. Some implementation issues (such as intelligent expansion of logical equivalence, pruning possible matings which previous work via symmetry implies will never extend to a mating, the use of connection graphs to find possible mates, and handling equality) are discussed. Finally, in the appendix, examples of theorems (some higher-order) proven are given. He notes that the procedure is complete for first-order logic, but not type theory.
This paper describes the higher order logic T of simply typed l-calculus formulas with the logical operators of negation (oo), disjunction (ooo), and the universal a-type set recognizer (o(oa)) and with the expected logical axioms. Then, expansion trees are defined and described, as well as operations for extending expansion trees by selection and expansions. An ET-proof of a formula A is an expansion tree with A as a shallow formula and a (boolean) tautology as a deep formula. A formula A is provable in T iff there exists an ET-proof of A (this is called "relative completeness"). He also gives a list representation of expansion trees.
He also describes how expansion trees can be used to complete incomplete natural deduction proofs.
Analytic proofs are resolution or mating proofs, and non-analytic proofs are natural deduction proofs. This paper describes natural deduction systems I and I* (I with a rule "Mix" which is a variant of "Cut") and expansion trees. He then describes how to construct I-proofs from expansion tree proofs and vice-versa (by giving a correspondence between children in trees and deduction rules). Expansion tree proofs can also be constructed from I*-proofs by first performing cut-elimination (i.e., eliminating each use of Mix--which he proves can be done using a double-induction). Unfortunately, a simple I*-proof can expand into an extremely long mix-free I-proof. A result by Statman (using an example from Combinatory Logic) shows that this is inevitable. Finally, he shows how to convert a resolution proof (with Skolem functions) into an expansion tree proof.
Expansion tree proofs for theorems of type theory (without extensionality, choice, and infinity) are introduced. An expansion tree proof is an expansion tree where the deep formula is tautologous and the dependency relation on expansion terms is acyclic. If a formula has an ET-proof, then it has an H-proof (Herbrand proof)--an H-proof is a deduction using tautologies as axioms, and anti-prenexing, existential and universal generalization, lambda expansion, and existential contraction as inference rules. This provides soundness of ET-proofs.
The author also shows how two [dual] expansion trees with the same shallow formula can be merged to give one whose deep formula is implied by the disjunction of the previous deep formulas [implies the conjunction of the previous deep formulas]. This is used to show how ET-proofs for [A or B] and [C or B] can be combined to give an ET-proof for [[A and C] or B]. Similarly, we can obtain an ET-proof for [A or B] from an ET-proof for [A or B or B]. Both of these results are used in the next section on sequential proofs.
A cut-free sequential proof calculus (in the spirit of Gentzen) is presented. The author also considers q-sequents of expansion trees (not just formulas) with dual expansion trees in the antecedent and expansion trees in the succedent, and where the combined expansion trees (with a disjunctive root node and negation nodes preceding the dual trees) is an ET-proof. The author shows how to convert an ET-proof into a sequential proof of the formula. Conversely, the author shows how to convert a sequential proof of a sequent to a q-sequent with the original sequent as shallow formulas (as a special case: formulas with sequential proofs have ET-proofs). This gives soundness and completeness of ET-proofs, as well as a direct method for translating between ET-proofs and more natural sequential proofs.
An ET-proof [P implies Q] of a formula [C implies D] gives a "linear" derivation (in the sense of Craig) which is "balanced"--that is, first we do universal instantiations and duplications and lambda contractions, then we do one propositional step ("matrix change"), and end with existential generalizations and simplifications and lambda expansions. As a result, we have a "propositional interpolant" X so that we can prove [C implies X] and [X implies D] and we have every parameter in X occurred either in D and some expansion term in P or in C and some expansion term in Q. (I'm not satisfied with the proof of this last statement.)
Finally, the author presents the appropriate way to handle Skolem terms (Skolem functions must have necessary arguments and these necessary arguments must not contain variables which become bound) and a notion of a Skolem expansion tree proof (ST-proof). The set of all formulas satisfying these restrictions forms the Herbrand universe. This set is closed under beta reduction. Skolem expansion trees remain Skolem expansion trees under substitution (which was not true of expansion trees). Also, we can dispense with the requirement that the dependency relation be acyclic because the equivalent embedding relation (on selected variables) is explicitly represented by subformulas (of Skolem terms). The author proves soundness and completeness of ST-proofs by showing how to translate back and forth from ET-proofs.
This article is reprented in the Festschrift for Peter B. Andrews
Several issues relating to type theoretical theorems and proofs are discussed in this paper. The author begins by showing how every theorem can be seen as a tautology disguised by operations. Finding a proof can be thought of as unmasking the disguise by reversing the operations. Tautologies and contradictions can be recognized by finding acceptable matings. Expansion trees can be used to expand theorems into tautologies, or negations of theorems into contradictions (which is how they are usually used). Expansion trees are defined and examples are given. Also, a criteria on selected variables [selected parameters] is given to ensure that an expansion proof is valid. This involves a certain transitive relation on selected variables being irreflexive. Skolemization can be used to ensure this, but one must be careful that Skolemization does not introduce the Axiom of Choice.
Procedures exist to translate expansion proofs into natural deduction proofs. Also, procedures exist to translate cut-free natural deduction proofs into expansion tree proofs. However, if a procedure were to exist to translate natural deduction proofs in general into expansion tree proofs, and we could formalize this procedure into analysis (type theory with the axioms of infinity, extensionality, and descriptions), then we could contradict Godel's Second Incompleteness Theorem by syntactically proving analysis is consistent. The author outlines this procedure.
He discusses the search for expansion proofs, giving examples. The point is to expand variables appropriately so that a mating can be found. The search for matings can be carried out largely in parallel, with each processor contributing to an incompatibility record (failure record) associated with a central connection graph. Also, the connections in the connection graph itself may be removed later if unification turns out to be impossible (recall that unification is undecidable here). Mainly, he discusses expansions. Expansions are not found merely by using unifications stemming from the mating process. The procedure must also substitute variables associated with expansion nodes with primitive substitutions, containing new logical connectives, quantifiers, or with projection terms. These primitive substitutions will contain new variables which will either be substituted later with more terms of one of these forms, or determined by unification from the mating process. Methods for choosing these primitive substitutions is a very important research area.
The mating method is reviewed (concentrating on the first-order fragment) and indexed expansion trees are defined. A total ordering is defined on nodes in a jform and on vertical paths. A path enumerator is defined by giving operations for constructing the cheapest extensions of path segments, most expensive extensions, successors and predecessors.
The main chapter describes path-focused duplication (in TPS, this corresponds to MS90-3). Mating search proceeds by choosing the next unspanned path and either expanding the mating (by choosing literals to mate) or duplicating an expansion node on the path. This splits the path into several paths to span, but the duplication is local so the total number of unspanned paths does not explode in the way it would if we made a global duplication. The duplications are implicit, in the sense that we do not actually duplicate in the expansion tree until we have a complete mating. Some experimental results are given in the next chapter.
Some optimizations are made in the propositional case (where duplication is not an issue).
Unification is extended in a way to check that the imbedding relation is guaranteed to be acyclic. (This can be seen as a natural extension of occurs-check in the first-order case.) Sunil uses graphs with 2-colored edges. The correctness of this assumes expansion terms are expansion variables, so that all terms are found using unification. This has been extended in TPS to include the case when terms are partially determined (e.g., by instantiating set variables in a pre-processing step). This is described in the TPS Programmer's Guide.
More intelligent backtracking could be achieved using maximally unifiable subsets and/or minimally ununifiable subsets of a mating. This is described, but has not been implemented.
Finally, dissolution for jforms is defined. This differs somewhat from Murray/Rosenthal dissolution. One of the reasons is because jforms are n-ary while semantic graphs are binary. There is an example that demonstrates that dissolution on a dissolution chain (special kind of partial mating) may not remove all vpaths spanned.
This article is reprented in the Festschrift for Peter B. Andrews
This is a paper which describes the TPS project. The paper gives a history of TPS. The paper gives an overview of TPS, including the relationship between natural deduction proofs and expansion proofs. It also discusses tactics and tacticals for finding natural deduction proofs and for building natural deduction proofs from expansion proofs. It then discusses the automatic search techniques for expansion proofs, including expansions using gensubs (partial instantiations of quantified variables with new variables which will hopefully be determined to correspond to a successful mating). The authors note that flexible literals (in the sense of Huet's unification algorithm) are much harder to deal with than rigid literals since they can unify with any other literal.
The authors then give the example proof of THM15B that if an interate of a function has a unique fixed point, then the function has a fixed point. The successful instantiations for an expansion proof are given (with some discussion of the search for the hardest instantiation), and the construction of a corresponding natural deduction proof is discussed. Finally, a list of definitions and theorems are given, along with performance results concerning the automatic proofs of the theorems.
This paper presents two examples designed to demonstrate the superiority of type theory over first-order logic with axiomatic set theory. The first example is the fixed point theorem (that if an iterate of a function has a unique fixed point, then the function has a fixed point) and shows how involved the proof of lemmas and construction of relevant classes can be using Godel's axioms. The same lemmas can be proven and classes can be constructed in a very straightforward manner simply by using lambda definitions in type theory. The other example is McCarthy's "Tough Nut" example (in which two opposite corner squares are deleted from a checkerboard and the goal is to prove it has no tiling). A type-theoretical proof of this problem is outlined. The proof involves defining a relation (BLACK) on every other square (as in a real checkerboard), defining a function which uses the assumed tiling to move around the black squares, and showing that this function is injective (hence, in some sense, there are an infinite number of black squares). The finiteness of the board is used to obtain a contradiction. This proof should scale well to larger checkerboards. Also, the authors note that this proof does not have the "subformula property."
This thesis describes LTP, a learning theorem prover which works in type theory. After proving a theorem, it generates reductions, methods, and demons from the theorem (and possibly from lemmas proved as subproofs). These are used in the search for proofs of later theorems.
LTP can also handle searches for disproofs, for examples, etc. The thesis goes into some detail about the database, the methods, and the goal tree.
This thesis describes the IPR theorem prover. The prover uses first order logic enhanced with set constructor notation and descriptions. The automatic proofs are performed using a tableau method (and breadth-first unification), but are displayed to the user in a sequent style. The tableau method includes rules for dealing with sets as well as applying theorems from a knowledge base (the epsilon-rule). Much of the user interface is in English (using format strings associated with predicates and theorems in the knowledge base).
This paper describes a procedure (with examples) which--given clauses, an interpretation satisfying those clauses, and a goal--from the interpretation we can build a "dependency graph" of grounded literals or bags of grounded literals which are true in the interpretation, where arrows are annotated with the clauses that allow us to infer the target from the source. To prove the "arrow" "A->B", we find a path in a dependency graph (or common path of several dependency graphs) and attempt to lift it into a proof using the clauses from the arrows on the path.
He applies this method to Horn clauses and uses case analysis to handle non-Horn clauses.
This method can also be used for equational inference, but it turns out that the most useful interpretations are those in which "equality" is interpreted as a congruence.
This paper concerns a system GROVER which uses a diagram to reduce a theorem proving problem to a group of lemmata. The system first matches the theorem to the diagram in such a way that the hypotheses & conclusion are represented. The system then partially orders the intermediate steps which are represented in the diagram in such a way that certain objects in the diagram (which represent existential objects) are proven to exist. These intermediate lemmata may be used, according to the partial order, to prove further steps until the final conclusion is proven. This process is applied to a "Diamond Lemma" which states that Local CR + Well-Foundedness of a relation implies Global CR.
When trying to prove a theorem (they concentrate on equality of functional programs) by mathematical induction, it is often necessary (in order for the induction step to work) to prove a more general result from which the specific theorem follows. This paper extends the rippling method for generating such generalizations. Essentially, we need the conclusion to be an instance of the inductive hypothesis. So, the only places they should differ are positions in which the inductive hypothesis has a universally quantified variable (these universally quantified variables are called "accumulator variables" and the corresponding positions in the conclusion are called "sinks"). The portions of the conclusion which do not correspond to the inductive hypothesis forms the "wavefronts." "Wave-rules" provide rewrite rules which can move wavefronts outward (less nested), sideways (if we move towards a sink), and inwards (more nested). The goal is to eliminate these wavefronts. This method of moving the wavefronts is called "rippling."
He distinguishes between primary and secondary wavefronts. Primary wavefronts are those for which a sideways wave-rule applies, but the application is blocked because the subterm in which the new wavefront occurs does not contain a sink. Other wavefronts are called secondary. We construct generalizations by introducing new accumulator variables (hence new sinks). We first introduce new accumulator variables (by introducing primary accumulator terms) so that primary wavefronts will not be blocked (i.e., so that the term blocking the application of the wave-rule will contain a new sink). We also introduce secondary accumulator terms corresponding to secondary wavefronts. Although second-order variables are introduced by this method, the instantiations of variables for primary accumulator terms are more constrained than for secondary.
Eventually we hope to find a generalization for which the waverules move the wavefronts into sinks. Once this happens, the content of the sinks gives the instantiations of the accumulator variables to apply the inductive hypothesis.
This paper defines an abstraction as an effective mapping from a language L1 one formal system S1 to a language L2 of another formal system S2, where a formal system S is a language L and a subset ("set of formulae") Q of L. He generally restricts himself to axiomatic formal systems in which "Q" is the set of theorems TH(S) determined by a set of axioms W and inference rules D. S1 is called the ground space of the abstractions, and S2 is called the abstract space.
They classify these abstractions based upon what properties they preserve. Namely, he defines the classifications:
TC-abstractions: a in TH(S1) <==> f(a) in TH(S2)
TD-abstractions: f(a) in TH(S2) ==> a in TH(S1)
TI-abstractions: a in TH(S1) ==> f(a) in TH(S2)
Most abstractions they describe are TI-abstractions. Also, they consider the set NTH(S) in an axiomatic formal system. This is the set of formulas which, if their negation is added to the set of axioms, we can deduce a contradiction. This allows us to consider the abstraction classifications:
NTC-abstractions: a in NTH(S1) <==> f(a) in NTH(S2)
NTD-abstractions: f(a) in NTH(S2) ==> a in NTH(S1)
NTI-abstractions: a in NTH(S1) ==> f(a) in NTH(S2)
They relates NT*-abstractions to T*-abstractions by considering systems with negation and negation-preserving abstractions.
They further consider abstraction classifications:
L/W-invariant abstraction: W2 = f(W1)
(otherwise it is an L/W-variant abstraction)
L/D-invariant abstraction: D2 = "f"(D1) [ie, apply f to hyp formulae and conclusion]
(otherwise it is an L/D-variant abstraction)
D-invariant abstraction: D2 is a subset of D1
(otherwise it is an D-variant abstraction)
They also define theory abstractions as abstractions which preserve logical connectives and quantifiers.
They then describe many well-known examples of abstractions and classify them with respect to the categories defined above. The examples include Abstrips, GPS, Plaisted's ordinary and weak abstractions [taking clauses to clause sets satisfying certain properties], Plaisted's generalization functions [which uses the inference rule "resolution + generalization"], propositional abstractions, predicate abstractions, domain abstractions, Herbrand's theorem, and semantic abstractions.
They go on to show (without using categorial terminology) that abstractions form a category with objects as formal systems and arrows as abstractions. They also show (roughly) that abstraction categories defined above are closed under composition.
They then show that TI*-abstractions can take consistent ground spaces to inconsistent abstract spaces. In fact, given a TI*-abstraction (on axiomatic formal systems), there exists a set of consistent axioms whose abstract space is inconsistent.
They order abstractions by f <= g where f and g have a common dom by:
f <= g iff [f(j) in TH(cod(f)) ==> g(j) in TH(cod(g))].
After defining equivalence of abstractions by f <= g and g <= f, they note that the ordering defines a complete lattice. Results concerning this ordering includes that if f and g have a common dom, f is TD, and g is TI, then f <= g (which implies that a chain begins with TD-abstractions, then TC-abstractions, ending with TI-abstractions).
(They also note that an ordering with dual results can be defined on f and g with a common dom by:
f <= g iff [f(j) in NTH(cod(f)) ==> g(j) in NTH(cod(g))].)
Finally, they describe methods for constructing TI-abstractions, especially theory abstractions which are defined by defining the mapping on constant symbols, function symbols, and predicate symbols.
A propositional theory has a Horn greatest lower bound and least upper bound. Computing these can be hard in the worst case. An example is given where the Horn LUB is of size O(2^n) where the original theory is of size n. However, once we have these approximations, deciding if a consequence follows from the theory or not can often be reduced to linear time.
This technique of finding such approximations is called "knowledge compilation" and creates both a TI- and TD-abstraction in the sense of Giunchiglia and Walsh. An introduction to this framework for knowledge complilation is contained in the paper "A General Framework for Knowledge Compilation" (Proceedings of the International Workshop on Processing Declarative Knowledge, July 1991) by the same authors. In this paper, they also discuss extensions of the propositional case.
The author begins by describing SL-resolution and giving examples of problems for which SL-resolution is inefficient. He then describes the connection graph procedure and shows how this procedure solves those problems.
The connection graph procedure involves taking a set of clauses (and their factors) and building a graph with literal occurrences as nodes and most general unifiers of literal occurrences as (undirected) links. A clause and all associated nodes and links are deleted if any one of its nodes/literals is pure (has no links/unifies with no complementary literals). The essential operation is selection of a link, deletion of the original link, creation of the associated resolvent (with all factors) and links inherited from the parent clauses which are compatible with the substitution associated with the selected link. More details are given in the paper.
The examples the author examines include a list sorting procedure and natural-language parsing.
The Map Calculus is an algebraic form of logic in the tradition of Peirce and Schroeder, revived by Tarski and Givant in 1987. The calculus is based on equations between binary relations over a given universe. The formulation in this paper takes intersection, and symmetric difference, composition, and inverse as primitive operations, and empty, full, and identity as basic relations. The axioms are not complete for ordinary set-valued semantics. A first order sentence can be translated into a map calculus equation if it is equivalent to a sentence involving three or fewer variables. A graph-based algorithm describes the translation. When a theory is strong enough to include some kind of pairing, then any sentence can be translated (using pairing to reduce the number of variables).
A few examples are formulated in Map Calculus: Lists, GB Set Theory, Finite Set Theory, and portions of Lattice Theory.
The decidable fragment of set theory considered in this paper is MLSS (Multi-Level Syllogistic with Singleton), containing membership, equality, subset, binary intersection, binary union, set difference, a finite set constructor, the empty set. Quantifiers are not allowed. First, a formula is normalized to be a set of conjunctions of literals of the form "x in y", "x not in y", "x = y", "x not= y", "z = x U y", etc. (essentially introducing variables to stand for more complex subterms). We work on these normalized forms. (The authors avoid such normalized forms in later work.) A collection of 12 tableau rules are given. The first 11 are used to "saturate" a branch of the tableau. Rule (12) is a sort of cut rule (distinguishing between the cases when two sets are equal or are not equal) and is only applied when a tableau is saturated and some branch is open. (A branch is closed if there is either a membership loop, or complimentary literals.) In such a case, a "realization" model is built for an open branch, and this is used to guide the application of Rule (12). So, we interleave saturation with a kind of model checking. (In later work, the authors avoid the expense of building models during search.)
The saturation steps terminate because no new subterms are created by rules (1) - (11). Also, Rule (12) cannot be applied an infinite number of times because each time the cut is on a formula "x = y" where x and y are variables in the original problem. So, this terminates.
Soundness follows easily by the soundness of the rules.
Completeness follows by showing that if a saturated tableau has an open branch, then there is a realization which does not satisfy some literal of the form "x not in y" or "x = y minus z" or "x not= y". In each case we can find two variables x and x' in the original problem on which we can apply Rule (12).
An example ("-[x = {y} and x = y U z] or [y = empty and x = z]") is given, but this example does not translate to type theory as it would be ill-typed.
This paper presents a different tableau-based decision procedure for MLSS (here reformulated slightly). One improvement is that we do not require normalization of the formula. Realizations are used to prove completeness, but are not explicitly constructed to guide the search. Instead the calculus is separated into saturation rules (which only apply when they do not introduce new subterms), and fulfilling rules (which apply when preconditions are met and the subsumption requirement is false). The fulfilling rules are designed to split the proof into exclusive cases, using variations of cut rules. (This is said to be an efficiency improvement over Smullyan style tableaux.)
The decision procedure consists of applying saturation rules until no more apply. If a branch is saturated and open, then the formula has a realization model. Otherwise, a fulfilling rule will apply to the branch and we continue. This procedure terminates because no new subterms are generated, so the number of literals the rules can generate is finite.
Soundness follows easily by the soundness of the rules.
Completeness follows by showing that a realization of an open and saturated branch is a model.
The same example (whose correspoding type theoretical statement is ill-typed) is given.
This is an extension of the decision procedure to
MLSSF-all (
Eighteen tableau rules are given, with restrictions designed to ensure termination. The two rules (13) and (18) introduce new subterms, but only in a restricted way.
An example is given (which makes what in type theory would be a non-trivial use of extensionality). This example, however, does not translate to type theory as it would be ill-typed.
Termination is shown by showing the number of terms, hence the number of literals, in the tableau is finite.
Soundness follows easily by soundness of the rules.
Finally, some efficiency issues are discussed. The branching factor can be minimized by adjusting the rules to encourage cuts. Also, it is argued that the saturation technique used in this paper is more efficient than generating models as in the earlier work.
The SCAN algorithm converts some second order formulas into equivalent first order formulas. The algorithm may not terminate, but if it does, then the result is equivalent - this is proven in the paper. See also the system description.
Other ideas for transforming second-order formulas into first-order formulas date back to Ackermann.
Example applications are given by circumscription, semantics of modal logics, and relating properties of relations to properties of corresponding functions.
SCAN ("Synthesizing Correspondence Axioms for Normal Logics") converts some second order formulas to equivalent first order formulas. Start with a second order formula of the form "exists P1 . . . exists Pn phi" where the Pi's are relations and phi is a first order formula. The idea is to put phi into clause normal form, skolemize, and form all C-resolvents and C-factors ("C" means "Constraints" - instead of unifying, we put diseqns as constraints on the result clause) which act on P-literals. When all such consequences are generated we can delete the original clause with the predicate P. If this terminates, we will have a set of clauses which do not mention the predicate variables. If we can unskolemize, then we get an equivalent first-order formula. This is proven correct in another paper by showing that the transformations preserve equivalence. It appears that if the resulting first-order sentence is satisfied by a model, the interpretation of the Pi's can be a finite set by listing the elements that should be in Pi (or, we can list finitely many elements which should not be in Pi, making it co-finite).
The system is implemented using OTTER as an inference system. First we enter the list of predicates, put the list of clauses using the predicates on the set of support, and put other clauses on the usable list. Syntactic tricks can be used to simulated C-resolution (e.g., change P(s) to "P(x) or ~x=s"). OTTER's output (if it terminates) should be a collection of clauses which SCAN might be able to unskolemize to get a first-order formula.
Two examples are considered: Finding first-order formulas equivalent to second order circumscription formulas, and finding conditions on the accessability relation (ie, the "later/higher world" relation on worlds) for modal logics which are equivalent to axioms in the modal logic. For example, "box p => p" implies the accessability relation is reflexive.
Set unification means solving systems of equations of the form {s1} U . . . U {sn} U S =? {t1} U . . . U {tm} U T. The notation used in the paper is {s1,...,sn|S}. Here S may be a set variable called the "tail", or may be the empty set. Note also that the terms si may themselves be set terms, so this generalizes well to type theory where we may have sets of sets. (This paper does assume foundation, which shows up as an occurs-check.) Set unification in general is NP-complete. The unification problem is finitary. Set unification can be encoded in such a way so that it becomes a special case of ACI-unification.
First, an algorithm is given for the special case when the tails are the empty set. The algorithm computes minimal total relations which induce the unifiers. The resulting set of unifiers is complete, but may not be a minimal set of unifiers. The worst case complexity is analyzed. The worst case is when each term is a distinct variable, so every minimal total relation induces a unifier. For example, if n=m=5, there are 2945 such relations. This is a better bound than the one given by AC-unification.
Then, an algorithm is built on top of this to handle the cases where one side of a disagreement pair has a tail setvar, where both sides of a disagreement pair have the same tail setvar, and where the sides of a disagreement pair have different tail setvars.
The algorithms are sound and complete and terminate.
We can induce a reduction relation on set theoretic atoms by t in {x|A(x)} reduces to A(t). Huet's algorithm is modified to unify set theoretic atoms with respect to this reduction relation. Aside from flexible and rigid cases, we also have abstract cases, where the atom is a redex. Reduction steps are done on the fly during the algorithm. Aside from set variables, there are also propositional variables introduced during the search. These propositional variables essentially have arguments. Only imitation is used to handle set variables (but something like projection is used for propositional variables). Ada-like pseudocode is used to give the algorithm.
An example of a theorem which cannot be proved by only using this unification algorithm is given. It appears that the problem can be solved using higher-order unification (via a projection) in TPS.