Automatic recognition of tractability in inference relations.
A procedure is given for recognizing sets of inference rules that generate polynomial time decidable inference relations. The procedure can automatically recognize the tractability of the inference rules underlying congruence closure. The recognition of tractability for that particular rule set constitutes mechanical verification of a theorem originally proved independently by Kozen and Shostak. The procedure is algorithmic, rather than heuristic, and the class of automatically recognizable tractable rule sets can be precisely characterized. A series of examples of rule sets whose tractability is nontrivial, yet machine recognizable, is also given. The technical framework developed here is viewed as a first step toward a general theory of tractable inference relations.
Introduction
Certain well known algorithms can be viewed as polynomial time decision
procedures for inference relations. For example, transitive closure determines
whether a formula of the form x ! y can be proven from given inequalities
and a transitivity axiom. The union-find procedure determines whether an
equality can be proven from given equations and the reflexivity, tran-
sitivity, and symmetry axioms of equality. The congruence closure procedure
determines whether an equality can be proven from a given set of equations
and the symmetry, reflexivity, transitivity, and congruence axioms of
equality [1]. Each of these algorithms can be viewed as a decision procedure
for the inference relation generated by a certain set of inference rules. This
paper identifies a general class of "local" rule sets. These rule sets have the
desirable property that the generated inference relation is polynomial time
decidable.
Consider a set R of inference rules and let 'R be the inference relation
generated by R, i.e., the relation such that \Sigma 'R \Phi if there exists a derivation
of \Phi from \Sigma using the rules in R. The rule set R is called local if whenever
\Sigma 'R \Phi there exists a local derivation of \Phi from \Sigma - a derivation is local if
every proper subexpression of a formula in the derivation is either a proper
subexpression of \Phi, a proper subexpression of a member of \Sigma, or appears
as a subexpression of an inference rule in R. One can show that, for any
rule set R, one can determine, in polynomial time in the size of \Sigma and \Phi,
whether or not there exists a local derivation of \Phi from \Sigma. If R is local, i.e.,
the existence of a derivation ensures the existence of a local derivation, then
the inference relation 'R is polynomial time decideable.
One can easily show that a rule set consisting of a single transitivity rule
is local. The same is true of the rule set underlying the union-find procedure,
i.e., the reflexivity, symmetry, and transitivity axioms of equality. The rule
set underlying congruence closure, i.e., the reflexivity, symmetry, transitivity,
and substitution axioms of equality, is also local, although the locality of this
rule set is more difficult to prove.
In addition to providing a theoretical framework for the study of a certain
class of polynomial time algorithms, local inference relations provide a tool
for the construction of general purpose automated reasoning systems. No
sound and complete set of inference rules for first order logic can be local
(every local relation is polynomial time decidable, but the entailment relation
for first order logic is undecidable). However, local inference rules can be used
to reduce proof length in first order proof systems. This can be done through
the construction of a Socratic sequent system [2]. A sequent is an expression
of the form \Sigma ' \Phi where \Sigma is a set of formulas and \Phi is a formula. If
\Sigma 'R \Phi then we say that a rule set R generates the sequent \Sigma ' \Phi. A
Socratic sequent system consists of two rule sets - a local rule set and a set
of sequent rules. A sequent generated by the local set is called "obvious". A
proof in a Socratic sequent system is a series of sequents where each sequent
is either obvious or is derivable from earlier sequents by one of the sequent
rules. Because obvious sequents can abbreviate long derivations, proofs in
a Socratic sequent system can be shorter than proofs in more traditional
systems. However, because the rule set generating obvious sequents is local,
the correctness of a proof can still be verified in polynomial time. Particular
Socratic sequent systems for set theory and first order logic are described
in [5] and [4]. It appears that the power of the local rule set in a Socratic
sequent system can be enhanced through the use of a nonstandard syntax for
first order logic. Aspects of the syntax of English under Mantague semantics
have been used to construct particularly powerful general purpose local rule
sets [2].
Determining the locality of an arbitrary rule set can be difficult - it is
not known whether locality, as a property of rule sets, is decidable. The main
result of this paper is that a certain subclass of local rule sets - the bounded
local rule sets - can be mechanically identified. More precisely, there exists
a procedure that, given an arbitrary rule set, will find a counter-example to
locality whenever the rule set is not local, construct a proof that the rule set is
bounded local whenever it is bounded local, and will fail to terminate in cases
where the rule set is local but not bounded local. The rule set consisting of
the reflexivity, symmetry, transitivity, and congruence axioms of equality is
bounded local so the locality of this rule set can be mechanically recognized
by the procedure given here. This amounts to mechanical verification of
a theorem given in [3], [8], and [7]. Several novel examples of non-trivial
bounded local rule sets are given in this paper, including a rule set based on
the syntax of English. An example is also given of a rule set that is local but
not bounded local.
Hopefully, the notion of locality described in this paper is a first step
toward a more general understanding of tractable rule sets. Several open
technical problems and several directions for further research, are discussed at
the end of the paper. A better understanding of tractable inference relations
will hopefully result in an improved technology for the construction of semi-automated
verification systems and a deeper understanding of inference in
general.
F

Figure

1: A tractable set of Boolean inference rules
Preliminary Definitions
This paper presents a general procedure for recognizing certain cases in which
a set of inference rules generates a computationally tractable inference rela-
tion. The first step in constructing such a procedure is to precisely define
the notion of an "inference rule". Figure 1 gives basic inference rules for the
Boolean connectives : and -. In these rules a question mark in front of a
indicates a variable that can be replaced by different expressions in
different applications of the rule. Variables in inference rules will be called
metavariables to distinguish them from variables of the underlying language.
Throughout the remainder of this paper we let B (for Boolean) denote
the set of inference rules given in figure 1. All Boolean expressions can be
written in terms of the two universal connectives : and -. The rule set B
expresses some, but not all, of the inferential properties of these connectives.
The inference relation generated by these rules is linear time decidable. Yet,
if the above inference rules are augmented by a simple case analysis sequent
rule, then the rules become complete for Boolean inference.
As another example of a set of inference rules, consider the following rules
for equality.
The rules 12, 13, and 14 express the symmetry, reflexivity, and transitivity
properties of equality respectively, while rule 15 expresses the substitutivity
of equals for equals. It is well known that congruence closure provides a
polynomial time decision procedure for the inference relation generated by
these equality rules. The precise notion of inference rule developed here is
not general enough to allow for the notation ": : :" used in rule 15. Fortu-
nately, however, any inference problem involving function symbols of more
than two arguments can be converted to an equivalent problem involving
function symbols of at most two arguments. For example, a function f of
three arguments can be replaced by two functions pair and f 0 such that
loss of generality, we can
replace rule 15 by the following two rules.
In the remainder of this paper we let E denote the rule set consisting of rules
12, 13, 14, 15a and 15b.
Different metavariables have different syntactic kinds. For example, the
metavariables that appear in the Boolean rule set B range over formulas,
while the rule set E has metavariables that range over terms and metavariables
that range over function symbols. The phrases "formula", "term", and
"monadic function" each refer to a particular syntactic kind.
syntactic kind is either a kind symbol or an expression
of the form oe 1 \Theta oe 2 and each oe i are
syntactic kinds.
An expression is either a constant symbol or metavari-
able of a given syntactic kind, or an application of the form
is an expression of kind oe 1
and each s i is an expression of kind oe i . In the latter case the
is an expression of kind - .
In first order predicate calculus, an ordinary constant symbol is just a
constant of kind term; a proposition symbol is a constant of kind formula;
a function symbol of is a constant of kind term
predicate symbol is a constant of kind term formula. The
Boolean connectives : and - are constants of kind
and formula \Theta formula ! formula respectively. Quantifier-free predicate
calculus is the language generated by a set of constants of type term, a set
of constants of type formula, a set of function symbols, a set of predicate
(including equality) and the Boolean connectives. An expression
sometimes be written as (ffi e
occasionally as e 1
The above definitions do not allow for quantified expressions. This paper
only discusses inference rules that do not involve quantification. Even without
quantifiers, a set of rules can still generate an undecidable or intractable
inference relation. On the other hand, the presence of quantifiers does not
necessarily prevent tractability. Tractable inference relations involving quantification
are discussed in [5] and [4]. A more general notion of locality will
be needed to construct a procedure for automatically recognizing tractability
in rule sets that involve quantification.
An expression of kind formula will be called a formula

An inference rule is an object of the form
\Theta
and \Theta are all formulas.
metavariable substitution is a mapping ae from
metavariables to expressions such that, for any metavariable ?x,
we have that ae(?x) is an expression of the same kind as ?x.
Definition: For any metavariable substitution ae, and any expression
s, we define ae(s) to be the result of replacing each metavari-
able in s by its image under ae. For any set of expressions \Upsilon, we
define ae(\Upsilon) to be the set
Observation: For any metavariable substitution ae, and any expression
s, ae(s) is an expression with the same syntactic kind as
s.
derivable from a set of formulas
\Sigma under inference rules R if there exists an inference rule
\Theta
in R, and a metavariable substitution ae, such that ae(\Psi 1
are all members of \Sigma and ae(\Theta) equals \Phi.
A derivation of \Phi from \Sigma is a sequence of formulas
such that each \Psi i is either a member of \Sigma, or is one-step
derivable under R from previous elements of the sequence,
and \Psi n is the formula \Phi. If there exists a derivation of \Phi from \Sigma
under rule set R then we write \Sigma 'R \Phi.
Note that 'R is the relation generated by R in the standard way.
We are interested in finding general properties of a rule set R that guarantee
that the corresponding inference relation 'R is polynomial time decidable.
One way of doing this is to consider a "restricted" relation ' R that is explicitly
constructed to be polynomial time decidable. This can be done using
the following terminology.
will be called a label formula of a set
of
expressions\Omega if every proper subexpression of \Psi is a member
of \Omega\Gamma
For any set of formulas \Gamma and rule set R we define
\Gamma) to be the set of all proper subexpressions of formulas in
plus all closed (variable-free) proper subexpressions of formulas
in R.
Note that, for any finite rule set R and finite formula set \Gamma, the
is finite. However, any formula constant or formula metavariable is a label
formula of any expression set. This implies that any expression set has
an infinite set of label formulas. In spite of the infinity of label formulas,
however, restricting the inference process to label formulas of a small finite
set yields a tractable inference relation.
We write \Sigma ' R \Phi if there exists some derivation
of \Phi from \Sigma under rule set R such that each \Psi i is
a label formula of \Omega\Gamma R; \Sigma [ f\Phig).
Tractability Lemma: For any finite rule set R, the relation ' R
is polynomial time decidable.
set of rules R will be called local if the relation
R is the same as the relation 'R .
The tractability lemma implies that the inference relation generated by a
local rule set is polynomial time decidable. The proof of a refined version of
the tractability lemma is given in appendix I. As an example, consider the
problem of determining whether or not \Sigma ' E \Phi where \Phi and each formula
in \Sigma is an equation between first order terms and E is the equality rule set
(rules 12, 13, 14, 15a and 15b). The expression
of the equality symbol plus all first order terms that appear in \Sigma and \Phi. If s
and t are terms in \Omega\Gamma E; \Sigma [ f\Phig) then the equation is a label formula
of \Omega\Gamma E; \Sigma [ f\Phig). Let n be the total size of \Sigma [ f\Phig. There are order n 2
equations that are label formulas of \Omega\Gamma E; \Sigma [ f\Phig). This implies that one
can enumerate, in polynomial time, all label formulas of \Omega\Gamma E; \Sigma [ f\Phig) that
can be derived from \Sigma using derivations restricted to label formulas.
The definition of locality does not provide any obvious way of determining
if a given rule set is local. Locality of the equality inference rules was
originally proved (using different terminology) independently by Kozen [3]
and Shostak [8]. Kozen uses a syntactic argument to show that if \Sigma 'E \Phi,
then \Phi. The proof is essentially an induction on the length of the
derivation used to establish \Sigma 'E \Phi. Shostak's proof of the locality of E
is semantic. Shostak observes that the relation ' E is clearly sound under
the standard semantics for equality. Furthermore, if \Sigma 6' E \Phi, then one can
construct a model of \Sigma in which \Phi is false. In other words, the relation ' E
is semantically complete. Since 'E is sound, and 'E is at least as strong as
the semantic completeness of ' E implies that ' E is the same as 'E . A
semantic proof using a simpler model construction was later given by Nelson
and Oppen [7].
Semantic proofs of locality are more compact in many cases than syntactic
proofs of the same results. However, it seems difficult to generalize semantic
proof techniques to the point where they can be used to mechanically recognize
a wide class of local rule sets. The following section shows that syntactic
techniques can be used to construct a general locality recognition procedure.
4 Syntactic Proofs of Locality
For any finite rule set R, the relation ' R is polynomial time decidable. The
rule set R is local if the relation ' R is the same as the relation ' R . A
general syntactic approach to proving locality for particular rule sets can be
constructed using the following definitions.
set of expressions \Upsilon will be called subexpression
closed if every subexpression of every member of \Upsilon is also a member
of \Upsilon.
R be a rule set, \Sigma a formula set, and let \Upsilon be
an expression set that is subexpression closed and that contains
as a subset. The set CR (\Sigma; \Upsilon) is defined to be the set of
formulas \Psi such that there exists a derivation of \Psi from \Sigma such
that every formula appearing in that derivation is a label formula
of \Upsilon.
f\Phig)).
We say that the set CR (\Sigma; \Upsilon) is universal if CR (\Sigma; \Upsilon)
contains all label formulas of \Upsilon.
Lemma: Let R be a fixed rule set. Let \Sigma be a formula set, let
\Upsilon be a subexpression closed set
\Sigma). One can
determine whether CR (\Sigma; \Upsilon) is universal in time polynomial in
the size of \Upsilon. If CR (\Sigma; \Upsilon) is not universal, it is finite and can be
enumerated in time polynomial in the size of \Upsilon.
The proof of the above lemma is not given here but is similar to the
proof of the refined tractability lemma given in appendix I. It is possible
to characterize locality in terms of the closure operator CR rather than the
inference relation ' R . To do this we need some additional terminology.
A one step extension of a subexpression closed set
\Upsilon is an expression ff that is not a member of \Upsilon but such that
every proper subexpression of ff is a member of \Upsilon.
An extension event for a rule set R is a four-tuple
\Upsilon? such that \Upsilon is subexpression closed and contains
is a one step extension of \Upsilon, and \Psi is a member of
The letters are used below to denote extension events.
Consider an extension event !ff; \Psi; \Sigma; \Upsilon?. Note that the formula \Psi may be
"old" in the sense that \Psi may be a member of CR (\Sigma; \Upsilon). Alternatively, \Psi
may be "new" in the sense that \Psi is a member of CR (\Sigma; \Upsilon [ fffg) but not
a member of CR (\Sigma; \Upsilon). The lemma given below states that a rule set R is
local if, and only if, it is impossible for a new formula to be a label formula
of the old set \Upsilon.
feedback event for a rule set R is an extension
event !ff; \Psi; \Sigma; \Upsilon? for R where \Psi is a label formula of \Upsilon but not
a member of CR (\Sigma; \Upsilon).
Lemma: A rule set R is local if, and only if, there are no feedback
events for R.
Proof: First, suppose there exists a feedback event E for R
with components !ff; \Psi; \Sigma; \Upsilon?. The fact that \Psi is a member
of CR (\Sigma; \Upsilon [ fffg) implies that \Sigma ' R \Psi. The fact that E is
a feedback event implies that \Psi is a label formula of \Upsilon but not
a member of CR (\Sigma; \Upsilon). The fact that \Psi is a label formula of \Upsilon
implies that \Upsilon
must not be a member
of CR (\Sigma; \Omega\Gamma R; \Sigma [ f\Psig)) and so \Sigma 6' R \Psi. Thus 'R and ' R are
different and R is not local.
The above argument shows that if R is local then there can
be no feedback events for R. We will now show the converse -
if there are no feedback events for R then R is local. Suppose
there are no feedback events for R. Now consider any \Sigma and
\Phi such that \Sigma 6' R \Phi. To show that R is local it suffices to
show that \Sigma 6' R \Phi. To show \Sigma 6' R \Phi it suffices to show that
for any finite subexpression closed set \Upsilon
\Phi) we have \Phi 62 CR (\Sigma; \Upsilon). By assumption we have that \Phi 62
CR (\Sigma; \Omega\Gamma R; \Sigma [ f\Phig)). Now let \Upsilon be any subexpression closed
set
such that \Phi 62 CR (\Sigma; \Upsilon). For any
one-step extension ff of \Upsilon we have that \Phi is not a member of
CR (\Sigma; \Upsilon [ fffg) - otherwise the tuple !ff; \Phi; \Sigma; \Upsilon? would be a
feedback event. By induction, this implies that \Phi is not a member
of CR (\Sigma; \Upsilon) for any finite subexpression closed set \Upsilon containing
thus \Sigma 6' R \Phi.
The above lemma reduces the problem of determining locality to the problem
of determining the existence of feedback events. The locality recognition
procedure is based on a general method of proving the non-existence of feed-back
events. This general method is best introduced using a simple example.
Consider the following rules expressing the monotonicity of an operator f .
Let M (for monotonicity) be this set of three inference rules. 1 We wish
to prove the non-existence of feedback events for M . Consider an extension
event !ff; \Psi; \Sigma; \Upsilon? for rules M . Either \Psi is an "old" formula, i.e., a member
of CM (\Sigma; \Upsilon), or \Psi is provable from old formulas using the above inference
rules. It is possible to characterize all the ways of proving a new formula
from old formulas using rules M . More specifically, for any extension event
one of the following four conditions must hold.
ffl \Psi is an "old" formula, i.e., a member of CM (\Sigma; \Upsilon).
ffl \Psi is the formula ff ' ff.
ffl ff is of the form f(s) and \Psi is a formula of the form ff ' t where
CM (\Sigma; \Upsilon) contains the formulas s ' u and f(u) ' t .
ffl ff is of the form f(s) and \Psi is a formula of the form t ' ff where
CM (\Sigma; \Upsilon) contains the formulas t ' f(u) and u ' s.
If an extension event satisfies one of the above conditions then either \Psi is an
old formula (the first condition) or \Psi contains ff as a proper subexpression
(the last three conditions). Thus \Psi is either an old formula, or \Psi is not a label
formula of \Upsilon. So no extension event satisfying one of the above conditions can
be a feedback event. The problem of proving the non-existence of feedback
events for M has now been reduced to the problem of proving that every
extension event for M satisfies one of the above four conditions. This can be
be done using the following definitions.
Let R be a rule set, \Sigma a formula set, \Upsilon a subexpression closed set
let ff be a one step extension of \Upsilon.
Definition: The set C ff;0
R (\Sigma; \Upsilon) is defined to be CR (\Sigma; \Upsilon). The
set C ff;j+1
R (\Sigma; \Upsilon) is defined to be C ff;j
R (\Sigma; \Upsilon) plus all label formulas
of \Upsilon [ fffg that can be derived from C ff;j
R (\Sigma; \Upsilon) via a single
application of an inference rule in R.
An in-depth analysis of the computational complexity of the relation 'M is given in
R (\Sigma; \Upsilon):
Consider a fixed but arbitrary \Sigma, \Upsilon and ff. To show the non-existence of
feedback events for M , it suffices to show that every formula \Psi in CM (\Sigma; \Upsilon [
fffg) satisfies one of the above four conditions with respect to \Sigma, \Upsilon, and ff.
The four conditions can be viewed as defining four different types of formulas
in the set CM (\Sigma; \Upsilon [ fffg). To prove that every formula in CM (\Sigma; \Upsilon [ fffg)
is of one of these four types, it suffices to prove, by induction on j, that
every formula in C ff;j
(\Sigma; \Upsilon) is of one of these four types. Every formula in
(\Sigma; \Upsilon) is an old formula and so is a formula of the first type. Now assume
that every formula in C ff;j
(\Sigma; \Upsilon) is of one of the four given types. Under this
assumption one can prove that every formula \Psi in C ff;j+1
(\Sigma; \Upsilon) is of one of
the given types. The induction step involves a case analysis on the proof rule
used to derive an element of C ff;j+1
M (\Sigma; \Upsilon) and the types of formulas used as
antecedents in the application of that rule.
The method just described for proving locality for the rule set M can be
generalized to a mechanical procedure for recognizing locality.
5 The Locality Recognition Procedure
The mechanical locality recognition procedure is not guaranteed to recognize
all local rule sets. However, it is possible to precisely characterize the class of
rule sets whose locality is mechanically recognizable by our procedure. This
precise characterization involves some additional terminology.
Definition: The rank of an extension event !ff; \Psi; \Sigma; \Upsilon? for a
rule set R is the least natural number j such that \Psi is an element
of C ff;j
R (\Sigma; \Upsilon).
Definition: For any natural number k and rule set R we say
that R is k-bounded-local if R is local and all extension events for
R have rank k or less. The rule set R is bounded-local whenever
there exists some k such that R is k-bounded-local.
Note that if R is k-bounded-local then CR (\Sigma; \Upsilon [ fffg) is always equal
to C ff;k
R (\Sigma; \Upsilon). It would seem that bounded-locality is an extremely strong
condition on inference rules and that few rule sets would satisfy this condi-
tion. However, all of the examples of local inference rules discussed above
are bounded-local - the rule sets E and M are 2-bounded-local while B
is 1-bounded local. Unfortunately, there are rule sets which are local but
not bounded-local. Let I consist of the reflexivity rule (16), transitivity rule
(17), plus rules 19, 20, and 21 given below. The rule set I is local but not
bounded-local (the proof is left as a non-trivial exercise for the reader).
19 "(?s; ?t) ' ?s
Given that I is local (although not bounded-local), the refined tractability
lemma implies that the generated inference relation is decidable in order n 3
time (the transitivity rule has order 3).
The following two theorems are the main results of this paper.
First Locality Recognition Theorem: For any rule set R and
bound k it is possible to determine whether or not R is k-bounded
local.
Second Locality Recognition Theorem: There exists a procedure
which, given any rule set R, does the following.
ffl If R is not local then the procedure terminates and outputs
a feedback event for R.
ffl If R is bounded-local, then the procedure terminates and
outputs the least k such that R is k-bounded-local plus an
enumeration of the possible "types" of extension events.
ffl If R is local, but not bounded-local, then the procedure fails
to terminate.
Consider the proof of locality for the monotonicity rules described in the
preceding section. The proof shows that every monotonicity extension event
falls into one of four types and that no extension event of these types can be
a feedback event. To mechanize this proof technique we need some way to
formally represent extension event types. Consider the third monotonicity
extension event type given in the preceding section:
ffl ff is of the form f(s) and \Psi is a formula of the form ff ' t where
CM (\Sigma; \Upsilon) contains the formulas s ' u and f(u) ' t .
The extension events of this type can be characterized by specifying the
form of ff, the form of \Psi, and certain formulas that must be in CR (\Sigma; \Upsilon).
In general, we allow a formal specification of an extension event type to
also include a specification of expressions that must be in \Upsilon. A formal
specification of an extension event type is a four-tuple !ff
ff 0 and \Psi 0 are patterns giving the form of ff and \Psi respectively; \Sigma 0 is a set of
formulas that must be included in CR (\Sigma; \Upsilon); and \Upsilon 0 is a set of expressions
that must be included in \Upsilon. The patterns ff 0 and \Psi 0 are just expressions
containing metavariables. The above type of monotonicity extension event
can be characterized by the following formal four-tuple.
The above four-tuple specifies the class of extension events in which ff
has the form f(?s), \Psi has the form ff ' ?t, and CR (\Sigma; \Upsilon) contains the
be the above four-
tuple. Note that \Upsilon 0 has been constructed so that \Upsilon 0 is a subexpression
closed set containing
is a one-step extension of \Upsilon 0 . In
fact, the tuple !ff all of the conditions given in the
definition of an extension event - this tuple is itself an extension event. In
general, an extension event containing metavariables defines an entire class
of "instantiations" of that extension event.
be an extension event !ff; \Psi; \Sigma; \Upsilon? and let
be an extension event We say that E is an
R-instance of the template E 0 , or that the template E 0 R-covers
the extension event E , if there exists a metavariable substitution
ae satisfying the following conditions.
We say that a template set T 1 R-covers an event set T 2 if every
member of T 2 is R-covered by some member of T 1 .
I will often say "covers" or "instance" rather than "R-covers" or "R-
instance" respectively when the rule set is clear from context. I will use
the term "event template", or just "template", rather than the term "exten-
sion event" to describe extension events that are being used as templates or
schemas for a whole class of extension events. The following lemmas state
useful properties of extension event templates.
Let E be !ff; \Psi; \Sigma; \Upsilon? and let E 0 be !ff
is an instance of E 0 by virtue of the metavariable substitution ae.
Lemma: The set ae(C R (\Sigma a subset of CR (\Sigma; \Upsilon).
Proof: Consider any formula \Theta in CR (\Sigma must show
that ae(\Theta) is a member of CR (\Sigma; \Upsilon). Consider a derivation D of \Theta
from \Sigma 0 such that all formulas in the derivation are label formulas
of \Upsilon 0 . Let ae(D) be the derivation derived from D by replacing
each expression in D by its image under the substitution ae. ae(D)
is a derivation of ae(\Theta) from ae(\Sigma 0 ). Furthermore, since ae(\Upsilon 0 ) is a
subset of \Upsilon, every formula in ae(D) is a label formula of \Upsilon. Since
every element of ae(\Sigma 0 ) is in CR (\Sigma; \Upsilon), we must have that ae(\Theta) is
also in CR (\Sigma; \Upsilon).
Lemma: For each natural number j, the set ae(C ff 0 ;j
subset of C ff;j
R (\Sigma; \Upsilon).
Proof: The proof is by induction on j. The previous lemma establishes
the result for Now assume that the result holds
for j and consider j \Theta be any formula in C ff 0 ;j+1
We must show that ae(\Theta) is in C ff;j+1
R (\Sigma; \Upsilon). \Theta is derivable, via a
single inference rule, from some formulas \Phi
By the induction hypothesis ae(\Phi are in C ff;j
R (\Sigma; \Upsilon).
But ae(\Theta) is derivable from ae(\Phi 1 ae(\Theta) is a label
formula of \Upsilon [ fffg. Thus ae(\Theta) is in C ff;j+1
R (\Sigma; \Upsilon).
Lemma: The rank of E is less than or equal to the rank of E 0 .
Proof: Let j be the rank of E 0 . The formula \Psi 0 is in C ff 0 ;j
By the above lemma, ae(\Psi 0 ) must be in C ff;j
R (\Sigma; \Upsilon). Since ae(\Psi 0 )
equals \Psi, the extension event E must have rank j or less.
is not a feedback event then E is not a feedback
event.
is not a feedback event the formula \Psi 0 is either
a member of CR (\Sigma or is not a label formula of \Upsilon 0 . In the
first case, the above lemma implies that ae(\Psi 0 ), and hence \Psi, is a
member of CR (\Sigma; \Upsilon). Now suppose that \Psi is not a label formula
of \Upsilon. Since \Psi 0 is a label formula of \Upsilon 0 [ fff 0 g but not a label
formula of \Upsilon 0 , the expression ff 0 must be a proper subexpression
of \Psi 0 . But this implies that ae(ff 0 ) is a proper subexpression of
thus ff is a proper subexpression of \Psi. This implies
that \Psi is not a label formula of \Upsilon and thus E is not a feedback
event.
The locality recognition procedure takes a bounded-local rule set R and
automatically constructs a proof of the locality of R using the same technique
as that used above in proving the locality of the rule set M . The proof of
locality of M involved showing that every extension event for M is an instance
of one of four specific templates. In order to construct an analogous proof for
an arbitrary bounded-local rule set R, the procedure must generate a finite
set of extension event templates, specific to the rule set R, and must show
that this finite set of extension event templates covers all extension events
for R. The recognition procedure uses a single process to both generate the
extension event templates and to prove that the generated templates cover
all extension events. This process starts with a set of "null" templates and
generates new templates by iteratively passing existing templates through
the inference rules.
Definition: The null template of kind - is !?ff; ?\Psi; f?\Psig; fg?
where ?ff is a metavariable of kind - .
An extension event has rank 0 if, and only if, it
is an instance of some null template.
Without loss of generality we can consider only the syntactic kinds used
in the inference rules, so we need only consider a finite set of null templates.
The following lifting lemma states the existence of a procedure for passing
templates through inference rules.
Lifting Lemma: Let R be a finite rule set and let T be a finite
template set such that T covers all extension events for R of rank
or less. It is possible to compute a finite template set R(T ) that
covers all extension events of rank less.
The proof of the lifting lemma, and a procedure for computing R(T ), is given
in appendix II.
Definition: For any rule set R, define T 0 (R) to be the set of null
templates and define T j+1 (R) to be T
covers every extension event for R with
rank j or less.
Lemma: R is local if, and only if, there is no j such that T j (R)
contains a feedback event.
Proof: Suppose there exists some feedback event for R. This
extension event must have some finite rank j and must be covered
by some element of T j (R). Templates that are not feedback events
2 A "more efficient" definition states that T j+1 (R) equals T j (R) plus those elements of
not already covered by some element of T j (R).
can not cover feedback events, so T j (R) must contain a feedback
event.
Lemma: R is j-bounded-local if, and only if, T j (R) does not
contain any feedback events, T j (R) covers R(T j (R)), and every
member of T j (R) has rank j or less. 3
Proof: First suppose T j (R) covers R(T j (R)). Since covering is
transitive, this implies that T j (R) covers all extension events of
less. But, by the same argument, this implies that
covers all extension events of rank or less. In fact,
covers all extension events. If, in addition, T j (R) does not
contain any feedback events, then there can be no feedback events
for R and R must be local. If all templates in T j (R) have rank
or less then, since no template can cover an extension event of
greater rank, all extension events for R must have rank j or less.
Now suppose that R is j-bounded local. Since there are no
feedback events for R, T j (R) must not contain a feedback event.
Since every extension event has rank j or less, T j (R) must cover
all extension events. This implies that T j (R) covers R(T j (R)).
Finally, since all extension events for R have rank j or less, every
template in T j (R) must have rank j or less.
The recognition theorems follow directly from the above lemmas. A procedure
based on the above lemmas has been implemented and all claims
made in this paper for the bounded-locality of particular rule sets have been
mechanically verified.
6 Additional Examples
This section presents additional examples of bounded-local rule sets. These
examples are intended to support the hypothesis that bounded-local rule sets
3 The most natural procedure for constructing R(T ) ensures that every extension event
in T j (R) has rank j or less.
are quite common and easily constructed. The examples are also intended
to support the hypothesis that recognizing locality is usually difficult.
Three examples of local rule sets are discussed above - a Boolean rule
set B, an equality rule set E, and a monotonicity rule set M . Additional
examples of bounded-local rule sets can be derived by considering various
unions of these rule sets, e.g., It turns out that
all such unions are bounded-local. In general, however, a union of local
rule sets need not be local. Similarly, a subset of a local rule set need not
be local. The locality of the various combinations of B, E, and M has
been determined through mechanical verification. Except for the rule set
B, which is 1-bounded-local, all combinations of rule sets B, E, and M are
2-bounded-local.
The next example is a rule set based on the syntactic structure of English
under Montague semantics. The rules involve expressions of three different
syntactic kinds: class expressions, specified noun phrases, and formulas.
The expressions can be given a simple semantics in which each class expression
denotes a set, each formula denotes a truth value, and each specified
noun phrase denotes an operator that maps sets to truth values (a second
order predicate). For example if x denotes a set, then (every x) is a specified
noun phrase and denotes a second order predicate that is true of a set
y just in case the set x is a subset of the set y - a formula of the form
((every x) y) is true just in case x ' y. Similarly, a formula of the form
((some x) y) is true just in case some element of the set x is a member
of the set y, i.e., just in case x " y is non-empty. For any binary relation
R, and class expression C, we let (R (some C)) and (R (every C))
be class expressions. For example, let kissed be a binary relation and let
man and woman be class expression constants. We have the class expressions
(kissed (some woman)) and (kissed (every woman)) and we have
formulas such as ((every man) (kissed (some woman))), or alternatively,
((some man) (kissed (every woman))). The meaning of expressions of the
form (R (some C)) and (R (every C)) can be defined so that the above
formulas have a natural meaning. The inference rules shown in figure 2 are
sound under this natural semantics.
Let N (for Natural) be the set of inference rules given in figure 2. It runs
22 ((every ?x) ?x)
((every ?x) ?y)
((every ?y) ?z)
((every ?x) ?z)
((some ?x) ?y)
((some ?y) ?x)
((some ?x) ?y)
((some ?x) ?x)
26 ((some ?x) ?y)
((every ?y) ?z)
((some ?x) ?z)
((every ?x) ?y)
((every (?R (some ?x))) (?R (some ?y)))
28 ((every ?x) ?y)
((every (?R (every ?y))) (?R (every ?x)))
29 ((some ?x) ?y)
((every (?R (every ?x))) (?R (some ?y)))

Figure

2: A Natural Rule Set
out that the rule set N is not local. However, the notion of locality can be
used to construct a polynomial time decision procedure for the relation 'N .
First, to see that N is not local, note that by combining inference rules 25
and
((some C) S) 'N ((every (R (every S))) (R (some C))):
However, the derivation the expression (some S) occurs as a proper subexpression
in a formula in the derivation and (some S) does not appear in the
statement of the inference problem so we have
((some C)S) 6' N ((every (R (every S))) (R (some C))):
In spite of the fact that N is not local, the locality recognition procedure
can be used to show that the relation 'N is polynomial time decidable. Let
N 0 be the rule set constructed from N by replacing formulas of the form
((every C) S) and ((some C) S) by formulas of the form (is-every C S)
and (is-some C S) respectively. For any formula \Phi and set of formulas
\Sigma we similarly define \Phi 0 and \Sigma 0 . We now have that \Sigma ' N \Phi if, and
only if, \Sigma 0 ' N 0
\Phi 0 . It now suffices to show that ' N 0
is polynomial time
decidable. But one can machine-verify the fact that N 0 is 4-bounded-local.
The refined tractability lemma then implies that there exists an order n 3
decision procedure for the relation 'N 0 .
Several technical questions remain unanswered. First, although the above
procedure shows that k-bounded locality is decidable for arbitrary rule sets,
it is not known whether (unbounded) locality is decidable. Another open
question regards inference relations rather than rule sets. An inference relation
will be called local if it is generated by some local rule set. It is possible
for a rule set R to be non-local and yet the relation 'R is generated by some
other rule set R 0 where R 0 is local - so the relation 'R can be local even
though R is not. Given a rule set R can one determine if the relation 'R
is local? We will say that a relation is k-bounded-local if it is generated by
some k-bounded-local rule set. Can one determine if 'R is k-bounded-local?
It seems likely that the definition of locality can be improved. Consider
the "natural" rule set N given above. This rule set is not local but a trivial
syntactic transformation yields an essentially equivalent, but bounded-local,
rule set N 0 . In general, replacing formulas of the form (P s t) by formulas
of the form ((P s) Currying the predicate P , can transform a local
rule set into one that is not local. The fact that locality is sensitive to
such trivial syntactic changes suggests that a more robust notion of locality
is possible. Ideally, a definition of locality should have the property that
locality of an arbitrary rule set is decidable, locality of a rule set guarantees
that the generated inference relation is polynomial time decidable, and the
class of local relations is closed under certain simple syntactic transformations
such as Currying.
An improved notion of locality might also lead to improvements in the
refined tractability lemma. Ideally, one should be able to mechanically recognize
that the Boolean inference relation is linear time decidable rather than
quadratic as the tractability lemma would indicate. Similarly, the single rule
of transitivity generates a relation that is decidable in linear time, rather
than cubic. In both of these examples the more efficient algorithm can be
viewed as a tighter restriction on forward chaining inference. Automatic
construction of a fast congruence closure algorithm is perhaps too much to
expect - fast congruence closure is not simply a matter of tightening the
restriction on forward chaining inference. However, it may be reasonable to
invoke special case mechanisms for rule sets that include the equality rules
as a subset. Hopefully, the framework presented in this paper is only a first
step toward a more powerful, and more general, theory of tractable inference
relations.



I: The Tractability Lemma
The tractability lemma states that for any finite rule set R, the relation
' R is polynomial time decidable. The statement of the tractability lemma
can be refined to give a useful upper bound on the order of the polynomial
involved. This refinement requires some additional terminology.
An inference rule r will be said to have order k
if there exist expressions e such that each e i is either a
metavariable or a proper subexpression of some formula in the
rule r, and such that every metavariable that appears in r also
appears in some e i .
For example, the rule
has order two because the two expressions
satisfy the requirements of the above conditions. Note that the rule does
not have order one because the equation ?f(?s not a
proper subexpression of a formula in the rule. Similarly, the rule
has order one, while the rule
has order two.
Refined Tractability Lemma: For a fixed finite rule set R, it
is possible to determine whether \Sigma ' R \Phi in order n k time where
n is the total size of \Sigma and \Phi and all rules in R have order k or
less.
Proof: For the purposes of this proof, a rule set R will be called normal if, for
every rule r in R, every metavariable in r appears as a proper subexpression
of some formula in r. We first reduce the problem of determining whether
\Sigma ' R \Phi to the the problem of determining whether \Sigma ' R \Phi in the case
where R is normal. If \Sigma is empty, and no inference rule in R has an empty
set of antecedents, then \Sigma 6' R \Phi. Thus we can assume without loss of
generality that either \Sigma is non-empty or some rule in R has no antecedents.
Consider a rule r and a metavariable ?\Psi that appears in r but does not
appear as a proper subexpression of any formula in r. The only place ?\Psi can
appear in r is as an antecedent or conclusion. If ?\Psi is both an antecedent
and a conclusion, then r can be removed from the rule set without affecting
the relation ' R . If ?\Psi is an antecedent but not a conclusion, then the above
comments about \Sigma and R imply that the rule r can be replaced by the rule
r 0 in which the antecedent ?\Psi has been removed. If ?\Psi is the conclusion of
r, but is not an antecedent of r, then we replace r by the rule r 0 derived from
r by replacing the conclusion ?\Psi with a new formula constant F . Let R 0 be
the rule set derived from R by making all such removals and replacements.
We now have that \Sigma ' R \Phi just in case \Sigma ' R 0 \Phi or \Sigma ' R 0 F . Furthermore,
R 0 is a normal rule set and all rules in R 0 have order k or less.
Now, without loss of generality, we can assume that R is a normal rule set.
Let \Upsilon be the
For a fixed rule set R, the set \Upsilon has order
elements. We have that \Sigma ' R \Phi just in case there exists a derivation
of \Phi from \Sigma under R such that each \Psi i is a label formula of
\Upsilon. Let r be an inference rule in R. For any metavariable substitution ae we
let ae(r) be the rule derived from ae by replacing each metavariable in r by its
image under ae. Since R is normal, we need only consider those instances ae(r)
where ae maps every metavariable in r to a member of \Upsilon. Let e be a set
of expressions that satisfy the conditions of the definition of r being order j.
Each e i is either a metavariable or a proper subexpression of some formula
in r. This implies that we need only consider those instances ae(r) where ae
is a substitution such that ae(e 1 are all members of \Upsilon. Since every
metavariable in r appears in some e i , the set of all such instances ae(r) can be
computed by matching the expressions e against elements of \Upsilon. For
a fixed rule r (independent of the size n), the set of all possible matches of
to elements of \Upsilon can be computed in order n j time. The restriction
that each ae(e i ) be an element of \Upsilon does not guarantee that the conclusion
and antecedents of ae(r) are label formulas of \Upsilon. Let I(r) be the set of all
such instances ae(r) such that the conclusion and all the antecedents of ae(r)
are label formulas of \Upsilon. The set I(r) can be computed in order n j time. Let
I(R) be the union of the sets I(r) for rules r in R. The set I(R) can be
computed in order n k time. We now have that \Sigma ' R \Phi just in case \Phi can
be derived from \Sigma under the rules I(R) by purely propositional reasoning
(we need not consider further substitution into the rules in I(R)). This is
equivalent to determining if a given proposition symbol can be derived from
a set of proposition symbols using a set of propositional Horn clauses. The
existence of such a derivation can be determined in time proportional to
the total size of the set of propositional Horn clauses. Since I(R) can be
computed in order n k time, its total size is order n k .



II: The Lifting Lemma
The lifting lemma can be stated as follows.
Lifting Lemma: Let R be a finite rule set and let T be a finite template set
such that T covers all extension events for R of rank j or less. It is possible
to compute a finite template set R(T ) that covers all extension events of rank
less.
The template set R(T ) can be constructed from R and T as follows.
R be a set of inference rules and let T be a set of extension
event templates such that any individual metavariable appears in at most one
rule or template (the rules and templates have all been resolved apart). We
define R(T ) to be the set of extension event templates that can be generated
non-deterministically by the following procedure.
1. Let
\Theta 1
\Theta n
be a rule in R and let !ff
in T such that there exists a metavariable substitution ae such
that ae(\Theta i
2. Let ae be the most general substitution satisfying the above conditions.
3. Let ff be the expression ae(ff i ) for any ff i .
4. Let fs be the set of all top level proper subexpressions of ae(\Phi),
i.e., proper subexpressions of ae(\Phi) that are not proper subexpressions
of any (larger) proper subexpression of ae(\Phi).
5. Let fu be disjoint sets whose union is
and such that there exists a substitution ae 0 such that ae 0
6. Let ae 0 be the most general substitution satisfying the above conditions
for the selected expressions um .
7. Let ff 0 be ae 0 (ff).
8. Let \Phi 0 be ae 0 (ae(\Phi)).
9. Let \Sigma 0 be ae 0 (ae( S
10. Let \Upsilon 0 be the least subexpression closed set containing all of the following

(a) All closed (variable-free) proper subexpressions of formulas that
appear in the rule set R.
(b) All proper subexpressions of \Sigma 0
(c) All sets of the form ae 0 (ae(\Upsilon i
(d) All proper subexpressions of ff 0 .
(e) The expressions ae 0 (w
11. If ff 0 is not a member of \Upsilon 0 then output !ff
If T is a set of extension event templates for R then R(T ) is also
a set of extension event templates for R and if all templates in T have rank
or less then all templates in R(T ) have less.
Proof: Let !ff some tuple in R(T ). An extension event
template is just an extension event (which may contain metavariables) so
we have to show that this tuple satisfies all of the conditions for being an
extension event for R. Step 10 ensures that \Upsilon 0 is subexpression closed and
steps 10a and 10b ensure that \Upsilon 0
and the
condition in step 11 that ff 0 not be in \Upsilon 0 , ensure that ff 0 is a one step extension
of \Upsilon 0 . Steps 3, 4, 5, 6, and 10e ensure that every immediate subexpression
of \Phi 0 is either a member of \Upsilon 0 or is equal to ff 0 . This guarantees that \Phi 0 is a
label formula of \Upsilon 0 [ ff 0 .
We must also show that the formula \Phi 0 is a member of C ff 0 ;j+1
be the templates in T selected at step
1 of the procedure. Let ae 00 be the substitution that maps every expression e to
ae 0 (ae(e)) where ae and ae 0 are the substitutions constructed in steps 2 and 6 re-
spectively. The construction of the substitution ae 0 ensures that \Phi 0 is derivable
from ae 00 (\Psi single inference rule. For each \Psi i we have that
\Psi i is a member of C ff;j
Now we show that ae 00 (CR (\Sigma
of CR (\Sigma \Theta be any formula in CR (\Sigma must show that ae 00 (\Theta)
is a member of CR (\Sigma 0 ; \Upsilon 0 ). Let D be a derivation of \Theta from \Sigma i such that every
formula in D is a label formula of \Upsilon i . ae 00 (D) is a derivation of ae 00 (\Theta) from
ae 00 (\Sigma). Furthermore, since every proper subexpression of every formula in D
is a member of \Upsilon i , every proper subexpression of every formula in ae 00 (D) is a
member of \Upsilon 0 . Thus ae 00 (\Theta) is a member of CR (\Sigma
is a subset of CR (\Sigma 0 ; \Upsilon 0 ). Since \Psi i is a member of C ff i ;j
a depth j derivation of ae 00 (\Psi i ) from ae 00 (CR (\Sigma
is a subset of CR (\Sigma 0 ; \Upsilon 0 ), there exists a depth j derivation of ae 00 (\Psi i ) from
argument similar to the one above shows that every formula
in this derivation is a label formula of \Upsilon 0 [fff 0 g and thus ae 00 (\Psi i ) is a member
of C ff 0 ;j
derivable in one step from ae 00 (\Psi
thus \Phi 0 must be a member of C ff 0 ;j+1
If T is a set of templates that covers all extension events with rank
or less, then R(T ) covers all extension events of rank j + 1.
be an extension event !ff 00 ; \Phi 00 ; \Sigma 00 ; \Upsilon 00 ? of rank j +1 (the use
of double primes allows the names used in this proof to agree with the names
used in the above procedure). By definition, \Phi 00 is a member of C ff;j+1
R (\Sigma; \Upsilon)
but not a member of C ff;j
R (\Sigma; \Upsilon). This implies that there exist formulas
in C ff 00 ;j
and an inference rule r of the form
\Theta 1
\Theta n
in R that allows \Phi 00 to be derived from \Psi 00
n by applying a substitution oe
to the inference rule. We have that oe(\Theta i
be the extension events !ff 00 ; \Psi 00
Each extension event E 00
i has rank j or less and thus each E 00
i is covered by some
template in T . Let
that cover extension events E 00
via substitutions ae respectively.
We have assumed that no metavariable appears in more than one of r,
Therefore we can define a substitution - such that for any metavariable
x, if x appears in r then - (x) equals oe(x); if x appears in E i then - (x) equals
ae i (x); otherwise - (x) equals x. We now have
Thus we have that - (\Theta
n. So the substitution - satisfies all of the conditions given in
step 1 of the procedure. Let ae be the most general substitution satisfying
these conditions, as constructed at step 2 of the procedure.
The substitution ae is at least as general as - . This implies that the
substitution - can be written as ae followed by another substitution - 0 , i.e.,
for any expression e we have that - (e) equals - 0 (ae(e)). Let ff be ae(ff i ) as
defined in step 3 of the procedure. Since - 0 (ae(ff i
ff 00 , we have that - 0 (ff) equals ff 00 . The expression - 0 (ae(\Phi)) equals - (\Phi) which
equals \Phi 00 . Thus - 0 (ae(\Phi)) is a label formula of \Upsilon 00 [ fff 00 g. This implies
that, for each immediate subexpression s of ae(\Phi), we have that - 0
equals ff 00 or is a member of \Upsilon 00 . Let be the set of all immediate
subexpression u of ae(\Phi) such that - 0 (u) equals ff 00 . Let be the
set of immediate subexpressions w of ae(\Phi) such that - 0 (w) is a member of
\Upsilon 00 . Note that for each u i we have that - 0
Thus - 0 is a substitution that satisfies the requirement of step 5. Let ae 0 be
the substitution defined in step 6 of the procedure, i.e., the most general
substitution such that ae 0
The substitution ae 0 is at least as general as - 0 . As before, this implies
that - 0 can be written as ae 0 followed by another substitution - 00 , i.e., for any
expression e, - 0 (e) equals - 00 (ae 0 (e)). We now have that for any expression e,
be defined as in steps 7, 8, 9,
and 10 of the procedure, and let E 0 be the tuple !ff We will now
show that E 0 is an extension event template that covers the original extension
event via the substitution - 00 . We have that - 00 (ff 0 ) equals
which equals ff 00 . Similarly, - 00 (\Phi 0 ) equals \Phi 00 . Furthermore, a case
analysis on steps 10a through 10d can be used to show that - 00 (\Upsilon 0 ) is a subset
of \Upsilon 00 . This implies that ff 0 is not a member of \Upsilon 0 , otherwise we would have
that - 00 (ff 0 ) is a member of - 00 (\Upsilon 0 ) and so ff 00 would be a member of \Upsilon 00 which
violates the original condition that ff 00 be a one-step extension of \Upsilon 00 . Since
ff 0 is not a member of \Upsilon 0 the tuple E 0 is output by the procedure and thus is
a member of R(T ). By the above lemma, E 0 is an extension event template.
Finally, we must show that - 00 (\Sigma 0 ) is a subset of CR (\Sigma 00 ; \Upsilon 00 ). The set - 00 (\Sigma 0 )
equals
subset of CR (\Sigma



--R

Variations on the common subexpression problem.
Natural language based inference procedures applied to schubert's steamroller.
Complexity of finitely presented algebras.
Taxonomic syntax for first order inference.
A Knowledge Representation System for Mathematics.
The computational complexity of taxononic inference.
Fast decision procedures based on congruence closure.
An algorithm for reasoning about equality.
--TR
Ontic: a knowledge representation system for mathematics
Taxonomic syntax for first order inference
Fast Decision Procedures Based on Congruence Closure
Variations on the Common Subexpression Problem
An algorithm for reasoning about equality
Complexity of finitely presented algebras

--CTR
Hubert Comon-Lundh , Vronique Cortier, Security properties: two agents are sufficient, Science of Computer Programming, v.50 n.1-3, p.51-71, March 2004
Hans Jrgen Ohlbach, Elimination of Self-Resolving Clauses, Journal of Automated Reasoning, v.20 n.3, p.317-336, June 1998
Rakesh Verma, Algorithms and reductions for rewriting problems. II, Information Processing Letters, v.84 n.4, p.227-233, November 2002
Harald Ganzinger, Efficient deductive methods for program analysis, ACM SIGPLAN Notices, v.36 n.3, p.102-103, March 2001
David Basin , Harald Ganzinger, Automated complexity analysis based on ordered resolution, Journal of the ACM (JACM), v.48 n.1, p.70-109, Jan. 2001
Stphanie Delaune, Easy intruder deduction problems with homomorphisms, Information Processing Letters, v.97 n.6, p.213-218, 31 March 2006
Robert Givan , David Mcallester, Polynomial-time computation via local inference relations, ACM Transactions on Computational Logic (TOCL), v.3 n.4, p.521-541, October 2002
David McAllester , Robert Givan, Taxonomic syntax for first order inference, Journal of the ACM (JACM), v.40 n.2, p.246-283, April 1993
Pascal Lafourcade, Intruder Deduction for the Equational Theory of Exclusive-or with Commutative and Distributive Encryption, Electronic Notes in Theoretical Computer Science (ENTCS), v.171 n.4, p.37-57, July, 2007
Javier Esparza , Andreas Podelski, Efficient algorithms for pre* and post* on interprocedural parallel flow graphs, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-11, January 19-21, 2000, Boston, MA, USA
Stphanie Delaune , Florent Jacquemard, A decision procedure for the verification of security protocols with explicit destructors, Proceedings of the 11th ACM conference on Computer and communications security, October 25-29, 2004, Washington DC, USA
Harald Ganzinger , Viorica Sofronie-Stokkermans , Uwe Waldmann, Modular proof systems for partial functions with Evans equality, Information and Computation, v.204 n.10, p.1453-1492, October 2006
Pascal Lafourcade , Denis Lugiez , Ralf Treinen, Intruder deduction for the equational theory of Abelian groups with distributive encryption, Information and Computation, v.205 n.4, p.581-623, April, 2007
Nancy Durgin , Patrick Lincoln , John Mitchell , Andre Scedrov, Multiset rewriting and the complexity of bounded security protocols, Journal of Computer Security, v.12 n.2, p.247-311, May 2004
Evgeny Dantsin , Thomas Eiter , Georg Gottlob , Andrei Voronkov, Complexity and expressive power of logic programming, ACM Computing Surveys (CSUR), v.33 n.3, p.374-425, September 2001
inference rules;machine inference;proof systems;proof theory;mechanical verification;automated reasoning;polynomial-time algorithm;theorem proving