Partial instantiation methods for inference in first-order logic

Satisfiability algorithms for propositional logic have improved enormously in recently years. This improvement increases the attractiveness of satisfiability methods for first-order logic that reduce the problem to a series of ground-level satisfiability problems. R. Jeroslow introduced a partial instantiation method of this kind that differs radically from the standard resolution-based methods. This paper lays the theoretical groundwork for an extension of his method that is general enough and efficient enough for general logic programming with indefinite clauses. In particular we improve Jeroslow's approach by (1) extending it to logic with functions, (2) accelerating it through the use of satisfiers, as introduced by Gallo and Rago, and (3) simplifying it to obtain further speedup. We provide a similar development for a "dual" partial instantiation approach defined by Hooker and suggest a primal-dual strategy. We prove correctness of the primal and dual algorithms for full first-order logic with functions, as well as termination on unsatisfiable formulas. We also report some preliminary computational results.

A low power, process invariant keeper design for high speed dynamic logic circuits

A low power keeper circuit using the concept of rate sensing has been proposed. The proposed technique reduces the amount of short circuit power dissipation in the domino gate by 70% compared to the conventional keeper technique. Also the total power-delay product is 26% lower compared to the previously reported techniques. The process tracking capability of the design enables the domino gate to achieve uniform delay across different process corners. This reduces the amount of short circuit power dissipation that occurs in the cascaded domino gates by 90%. The use of the proposed technique in the read path of a register file reduces the energy requirement by 26% as compared to the other keeper techniques. The proposed technique has been prototyped in 130nm CMOS technology.

Unified Vdd Vth Optimization Based DVFM Controller for a Logic Block

In this paper analytical expressions for optimal Vdd and Vth to minimize energy for a given speed constraint are derived. These expressions are based on the EKV model for transistors and are valid in both strong inversion and sub threshold regions. The effect of gate leakage on the optimal Vdd and Vth is analyzed. A new gradient based algorithm for controlling Vdd and Vth based on delay and power monitoring results is proposed. A Vdd-Vth controller which uses the algorithm to dynamically control the supply and threshold voltage of a representative logic block (sum of absolute difference computation of an MPEG decoder) is designed. Simulation results using 65 nm predictive technology models are given.

A decidable temporal logic with repeating values

Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this paper, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an infinite set is repeated in the future or in the past. Such a restriction has been inspired by a recent work on spatio-temporal logics. We show decidability of finitary and infinitary satisfiability by reduction into the verification of temporal properties in Petri nets. This is a surprising result since the logic is closed under negation, contains future-time and past-time temporal operators and can express the nonce property and its negation. These ingredients are known to lead to undecidability with a more liberal use of the freeze quantifier.

Digital Dead Time Logic and Protection Circuitry for PWM Voltage Source Converters

Power semiconductor devices have finite turn on and turn off delays that may not be perfectly matched. In a leg of a voltage source converter, the simultaneous turn on of one device and the turn off of the complementary device will cause a DC bus shoot through, if the turn off delay is larger than the turn on delay time. To avoid this situation it is common practice to blank the two complementary devices in a leg for a small duration of time while switching, which is called dead time. This paper proposes a logic circuit for digital implementation required to control the complementary devices of a leg independently and at the same time preventing cross conduction of devices in a leg, and while providing accurate and stable dead time. This implementation is based on the concept of finite state machines. This circuit can also block improper PWM pulses to semiconductor switches and filters small pulses notches below a threshold time width as the narrow pulses do not provide any significant contribution to average pole voltage, but leads to increased switching loss. This proposed dead time logic has been implemented in a CPLD and is implemented in a protection and delay card for 3- power converters.

Fuzzy logic based TCSC supplementary controller for damping of inter area oscillations in power system

This paper describes an application of a FACTS supplementary controller for damping of inter area oscillations in power systems. A fuzzy logic controller is designed to regulate a thyristor controlled series capacitor (TCSC) in a multimachine environment to produce additional damping in the system. Simultaneous application of the excitation controller and proposed controller is also investigated. Simulation studies have been done with different types of disturbances and the results are shown to be consistent with the expected performance of the supplementary controller.

An Optimal Fuzzy Logic Controller tuned with Artificial Immune System

In this paper, a method for the tuning the membership functions of a Mamdani type Fuzzy Logic Controller (FLC) using the Clonal Selection Algorithm(CSA) a model of the Artificial Immune System(AIS) paradigm is examined. FLC's are designed for two problems, firstly the linear cart centering problem and secondly the highly nonlinear inverted pendulum problem. The FLC tuned by AIS is compared with FLC tuned by GA. In order to check the robustness of the designed PLC's white noise was added to the system, further, the masses of the cart and the length and mass of the pendulum are changed. The PLC's were also tested in the presence of faulty rules. Finally, Kruskal Wallis test was performed to compare the performance of the GA and AIS. An insight into the algorithms are also given by studying the effect of the important parameters of GA and AIS.

Dual enzyme responsive microcapsules simulating an ``OR'' logic gate for biologically triggered drug delivery applications

Hollow microcapsules capable of disintegrating in response to dual biological stimuli have been synthesized from two FDA approved drug molecules. The capsules fabricated from protamine and chondroitin sulphate disintegrate in the presence of either trypsin or hyaluronidase enzymes, which are documented to be simultaneously over-expressed under some pathological conditions.

Gene expression programming-fuzzy logic method for crop type classification

Crop type classification using remote sensing data plays a vital role in planning cultivation activities and for optimal usage of the available fertile land. Thus a reliable and precise classification of agricultural crops can help improve agricultural productivity. Hence in this paper a gene expression programming based fuzzy logic approach for multiclass crop classification using Multispectral satellite image is proposed. The purpose of this work is to utilize the optimization capabilities of GEP for tuning the fuzzy membership functions. The capabilities of GEP as a classifier is also studied. The proposed method is compared to Bayesian and Maximum likelihood classifier in terms of performance evaluation. From the results we can conclude that the proposed method is effective for classification.