Abstract Unlike other methods for theorem proving modulo with constrained clauses [12, 13], equational theorem proving modulo with constrained clauses along with its simplification techniques has not been well studied. We introduce a basic paramodulation calculus modulo equational theories E satisfying certain properties of E and present a new framework for equational theorem proving modulo E with constrained clauses. We propose an inference rule called Generalized E-Parallel for constrained clauses, which makes our inference system completely basic, meaning that we do not need to allow any paramodulation in the constraint part of a constrained clause for refutational completeness. We present a saturation procedure for constrained clauses based on relative reducibility and show that our inference system including our contraction rules is refutationally complete.

Rewriting modulo equations has been researched for several decades but due to the lack of suitable orderings, there are some limitations to rewriting modulo permutation equations. Given a finite set of permutation equations E, we present a new RPO-based ordering modulo E using (permutation) group actions and their associated orbits. It is an E-compatible reduction ordering on terms with the subterm property and is E-total on ground terms. We also present a completion and ground completion method for rewriting modulo a finite set of permutation equations E using our ordering modulo E. We show that our ground completion modulo E always admits a finite ground convergent (modulo E) rewrite system, which allows us to obtain the decidability of the word problem of ground theories modulo E.

Abstract We consider the problem of the unification modulo an equational theory associativity and commutativity (ACh), which consists of a function symbol h that is homomorphic over an associative–commutative operator +. Since the unification modulo ACh theory is undecidable, we define a variant of the problem called bounded ACh unification. In this bounded version of ACh unification, we essentially bound the number of times h can be applied to a term recursively and only allow solutions that satisfy this bound. There is no bound on the number of occurrences of h in a term, and the + symbol can be applied an unlimited number of times. We give inference rules for solving the bounded version of the problem and prove that the rules are sound, complete, and terminating. We have implemented the algorithm in Maude and give experimental results. We argue that this algorithm is useful in cryptographic protocol analysis.

A number of new cryptographic protocols are being designed to secure applications such as video-conferencing and electronic voting. Many of them rely upon cryptographic functions with complex algebraic properties that must be accounted for in order to be correctly analyzed by automated tools. Maude-NPA is a cryptographic protocol analysis tool based on narrowing and typed equational unification which takes into account these algebraic properties. It has already been used to analyze protocols involving bounded associativity, modular exponentiation, and exclusive-or. All of the above can be handled by the same general variant-based equational unification technique. However, there are important properties, in particular homomorphic encryption, that cannot be handled by variant-based unification in the same way. In these cases the best available approach is to implement specialized unification algorithms and combine them within a modular framework. In this paper we describe how we apply this approach within Maude-NPA, with respect to encryption homomorphic over a free operator. We also describe the use of Maude-NPA to analyze several protocols using such an encryption operation. To the best of our knowledge, this is the first implementation of homomorphic encryption of any sort in a tool for verifying the security of a protocol in the presence of active attackers.

We address the insecurity problem for cryptographic protocols, for an active intruder and a bounded number of sessions. The protocol steps are modeled as rigid Horn clauses, and the intruder abilities as an equational theory. The problem of active intrusion -- such as whether a secret term can be derived, possibly via interaction with the honest participants of the protocol -- is then formulated as a Cap Unification problem. Cap Unification is an extension of Equational Unification: look for a cap to be placed on a given set of terms, so as to unify it with a given term modulo the equational theory. We give a decision procedure for Cap Unification, when the intruder capabilities are modeled as homomorphic encryption theory. Our procedure can be employed in a simple manner to detect attacks exploiting some properties of block ciphers.

Front matter including table of contents, author list, PC list, and reviewer list.

Marine diesel engines operate in highly dynamic and uncertain environments, hence they require robust and accurate speed controllers that can handle the encountered uncertainties. Type-2 fuzzy logic controllers (FLCs) have shown that they can handle such uncertainties and give a superior performance to the existing commercial controllers. However, there are a number of computational bottlenecks that pose as significant barriers to the widespread deployment of type-2 FLCs in commercial embedded control systems. This paper explores the use of parallel hardware implementations of interval type-2 FLC as a means to eradicate these barriers thus producing bespoke co-processors for a soft core implementation of a FPGA based 32 bit RISC micro-processor. These coprocessors will perform functions such as fuzzification and type reduction and are currently utilised as part of a larger embedded interval type-2 fuzzy engine management system (T2FEMS). Numerous timing comparisons were undertaken between the co-processors and their sequential counterparts where the type-2 co-processors reduced significantly the computational cycles required by the type-2 FLC. This reduction in computational cycles allowed the T2FEMS to produce faster control responses whilst offering a superior control performance to the commercial engine management systems. Thus the proposed co-processors enable us to fully explore the potential of interval and possibly general type-2 FLCs in commercial embedded applications.

Marine diesel engines operate in highly dynamic and uncertain environments, hence they require robust and accurate speed controllers that can handle the encountered uncertainties. Type-2 Fuzzy Logic Controllers (FLCs) can handle such uncertainties; however they have a computational overhead associated with the iterative type-reduction process which can diminish the FLC real-time performance. Furthermore, manually designing a type-2 FLC is a difficult task particularly as the number of membership function parameters and rules increase. In this paper, we will introduce an embedded Real-Time Type-2 Neuro-Fuzzy Controller (RT2NFC) which overcomes the iterative type-reduction overhead and learns the parameters of interval type-2 FLC for marine engines. We have performed numerous experiments on a real diesel engine testing platform in which we compared our RT2NFC to a T2NFC based on the iterative type reduction procedure. Both T2NFCs were embedded on an industrial microcontroller platform where they handled the uncertainties to produce accurate and robust speed controllers that outperformed the currently used commercial engine controller. The RT2NFC gave approximately the same control response as the T2NFC, whilst the RT2NFC avoided the type-reduction overhead thus giving a faster real-time response.

Marine propulsion and traction diesel engines operate in highly dynamic and uncertain environments. The current speed controllers for marine/traction diesel engines are based on PID and type-1 fuzzy logic controllers (FLCs) which cannot fully handle the uncertainties associated with such dynamic environments. Type-2 FLCs can handle such uncertainties to produce a better control performance. However, type-2 FLCs have a computational overhead associated with the iterative type-reduction process which can reduce the FLC real-time performance, especially when operating on industrial embedded controllers which have limited computational and memory capabilities. In this paper, we introduce a real-time type-2 FLC that is suited for embedded controllers operating in marine/traction diesel engines. We have conducted numerous experiments where the embedded type-2 FLCs dealt with the uncertainties in real-time and displayed a robust control response that outperformed the PID and type-1 FLCs whilst using smaller rule bases

We give a set of inference rules with constant constraints. Then we show how to extend a set of equational clauses, so that if the application of these inference rules halts on these clauses, then the theory is decidable by applying a standard set of Paramodulation inference rules. In addition, we can determine the number of clauses generated in this decision procedure. For some theories, such as the theory of lists, there are 0(n /spl times/ lg(n)) clauses. For others it is polynomial. And for others it is simply exponential such as the theory of (extensional) arrays.

We give a new simplification method, called E-cycle Simplification, for Basic Completion inference systems. We prove the completeness of Basic Completion with E-cycle Simplification. We prove that E-cycle Simplification is strictly stronger than the

The resolution (and paramodulation) inference systems are theorem proving procedures for first-order logic (with equality), but they can run exponentially long for subclasses which have polynomial-time decision procedures, as in the case of SLD resolution and the Knuth-Bendix completion procedure, both in the ground case. Specialized methods run in polynomial time, but have not been extended to the full first-order case. We show a form of paramodulation which does not copy literals, which runs in polynomial time for the ground case of the following four subclasses: Horn clauses with any selection rule, any set of unit equalities (this includes completion), equational Horn clauses with a certain selection rule, and conditional narrowing.

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

This paper studies completion in the case of equations with constraints consisting of first-order formulae over equations, disequations, and an irreducibility predicate. We present several inference systems which show in a very precise way how to take advantage of redundancy notions in this framework. A notable feature of these systems is the variety of trade-offs they present for removing redundant instances of the equations involved in an inference. The irreducibility predicates simulate redundancy criteria based on reducibility (such as prime superposition and Blocking in Basic Completion) and the disequality predicates simulate the notion of subsumed critical pairs; in addition, since constraints are passed along with equations, we can perform hereditary versions of all these redundancy checks. This combines in one consistent framework stronger versions of all practical critical pair criteria. We also provide a rigorous analysis of the problem with completing sets of equations with initial constraints. Finally, an interesting consequence concerning the recalculation of critical pairs in completion procedures is discussed.