Mechanising first-order temporal resolution

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. Although a complete and correct resolution-style calculus has already been suggested for this specific fragment, this calculus involves constructions too complex to be of practical value. In this paper, we develop a machine-oriented clausal resolution method which features radically simplified proof search. We first define a normal form for monodic formulae and then introduce a novel resolution calculus that can be applied to formulae in this normal form. By careful encoding, parts of the calculus can be implemented using classical first-order resolution and can, thus, be efficiently implemented. We prove correctness and completeness results for the calculus and illustrate it on a comprehensive example. An implementation of the method is briefly discussed.

Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. In this paper, we develop a clausal resolution method for the monodic fragment of first-order temporal logic over expanding domains. We first define a normal form for monodic formulae and then introduce novel resolution calculi that can be applied to formulae in this normal form. We state correctness and completeness results for the method. We illustrate the method on a comprehensive example. The method is based on classical first-order resolution and can, thus, be efficiently implemented.

Equality and Monodic First-Order Temporal Logic

It has been shown recently that monodic first-order temporal logic without functional symbols but with equality is incomplete, i.e., the set of the valid formulae of this logic is not recursively enumerable. In this paper we show that an even simpler fragment consisting of monodic monadic two-variable formulae is not recursively enumerable.

Short-term temporal changes of soil carbon losses after tillage described by a first-order decay model

Tillage stimulates soil carbon (C) losses by increasing aeration, changing temperature and moisture conditions, and thus favoring microbial decomposition. In addition, soil aggregate disruption by tillage exposes once protected organic matter to decomposition. We propose a model to explain carbon dioxide (CO2) emission after tillage as a function of the no-till emission plus a correction due to the tillage disturbance. The model assumes that C in the readily decomposable organic matter follows a first-order reaction kinetics equation as: dC(sail)(t)/dt = -kC(soil)(t) and that soil C-CO2 emission is proportional to the C decay rate in soil, where C-soil(t) is the available labile soil C (g m(-2)) at any time (t). Emissions are modeled in terms soil C available to decomposition in the tilled and non-tilled plots, and a relationship is derived between no-till (F-NT) and tilled (F-Gamma) fluxes, which is: F-T = a1F(NT)e(-a2t), where t is time after tillage. Predicted and observed fluxes showed good agreement based on determination coefficient (R-2), index of agreement and model efficiency, with R-2 as high as 0.97. The two parameters included in the model are related to the difference between the decay constant (k factor) of tilled and no-till plots (a(2)) and also to the amount of labile carbon added to the readily decomposable soil organic matter due to tillage (a,). These two parameters were estimated in the model ranging from 1.27 and 2.60 (a(1)) and - 1.52 x 10(-2) and 2.2 x 10(-2) day(-1) (a(2)). The advantage is that temporal variability of tillage-induced emissions can be described by only one analytical function that includes the no-till emission plus an exponential term modulated by tillage and environmentally dependent parameters. (C) 2008 Elsevier B.V. All rights reserved.

Short-term temporal changes of bare soil CO2 fluxes after tillage described by first-order decay models

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Performance characteristics of high performance liquid chromatography, first order derivative UV spectrophotometry and bioassay for fluconazole determination in capsules

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Efeitos de acoplamentos biquadráticos e campos aleatórios em vidros de spins

In this work we have studied the effects of random biquadratic and random fields in spin-glass models using the replica method. The effect of a random biquadratic coupling was studied in two spin-1 spin-glass models: in one case the interactions occur between pairs of spins, whereas in the second one the interactions occur between p spins and the limit p > oo is considered. Both couplings (spin glass and biquadratic) have zero-mean Gaussian probability distributions. In the first model, the replica-symmetric assumption reveals that the system presents two pha¬ses, namely, paramagnetic and spin-glass, separated by a continuous transition line. The stability analysis of the replica-symmetric solution yields, besides the usual instability associated with the spin-glass ordering, a new phase due to the random biquadratic cou¬plings between the spins. For the case p oo, the replica-symmetric assumption yields again only two phases, namely, paramagnetic and quadrupolar. In both these phases the spin-glass parameter is zero. Besides, it is shown that they are stable under the Almeida-Thouless stability analysis. One of them presents negative entropy at low temperatures. We developed one step of replica simmetry breaking and noticed that a new phase, the biquadratic glass phase, emerge. In this way we have obtained the correct phase diagram, with.three first-order transition lines. These lines merges in a common triple point. The effects of random fields were studied in the Sherrington-Kirkpatrick model consi¬dered in the presence of an external random magnetic field following a trimodal distribu¬tion {P{hi) = p+S(hi - h0) +Po${hi) +pS(hi + h0))- It is shown that the border of the ferromagnetic phase may present, for conveniently chosen values of p0 and hQ, first-order phase transitions, as well as tricritical points at finite temperatures. It is verified that the first-order phase transitions are directly related to the dilution in the fields: the extensions of these transitions are reduced for increasing values of po- In fact, the threshold value pg, above which all phase transitions are continuous, is calculated analytically. The stability analysis of the replica-symmetric solution is performed and the regions of validity of such a solution are identified

Double sampling (x)over-bar control chart for a first-order autoregressive moving average process model

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

An existence theorem for an analytic first order PDE in the framework of Colombeau's theory

We study the existence of a holomorphic generalized solution u of the PDE[GRAPHICS]where f is a given holomorphic generalized function and (alpha (1),...alpha (m)) is an element of C-m\{0}.

First-order actions: A new view

We analyse systems described by first-order actions using the Hamilton-Jacobi (HJ) formalism for singular systems. In this study we verify that generalized brackets appear in a natural way in HJ approach, showing us the existence of a symplectic structure in the phase space of this formalism.

Electromagnetic field at finite temperature: A first order approach

In this work we study the electromagnetic field at finite temperature via the massless DKP formalism. The constraint analysis is performed and the partition function for the theory is constructed and computed. When it is specialized to the spin 1 sector we obtain the well-known result for the thermodynamic equilibrium of the electromagnetic field. (c) 2006 Elsevier B.V. All rights reserved.