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.

Towards First-Order Temporal Resolution

In this paper we show how to extend clausal temporal resolution to the ground eventuality fragment of monodic first-order temporal logic, which has recently been introduced by Hodkinson, Wolter and Zakharyaschev. While a finite Hilbert-like axiomatization of complete monodic first order temporal logic was developed by Wolter and Zakharyaschev, we propose a temporal resolution-based proof system which reduces the satisfiability problem for ground eventuality monodic first-order temporal formulae to the satisfiability problem for formulae of classical first-order logic.

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)

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.

Hamilton-Jacobi approach for first order actions and theories with higher derivatives

In this work, we analyze systems described by Lagrangians with higher order derivatives in the context of the Hamilton-Jacobi formalism for first order actions. Two different approaches are studied here: the first one is analogous to the description of theories with higher derivatives in the hamiltonian formalism according to [D.M. Gitman, S.L. Lyakhovich, I.V. Tyutin, Soviet Phys. J. 26 (1983) 730; D.M. Gitman, I.V. Tyutin, Quantization of Fields with Constraints, Springer-Verlag, New York, Berlin, 1990] the second treats the case where degenerate coordinate are present, in an analogy to reference [D.M. Gitman, I.V. Tyutin, Nucl. Phys. B 630 (2002) 509]. Several examples are analyzed where a comparison between both approaches is made. (C) 2007 Elsevier B.V. All rights reserved.

First order reversal curve analysis of nanocrystalline Pd80Co20 alloy films

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

Fish assemblage structure in a first order stream, southeastern Brazil: longitudinal distribution, seasonality, and microhabitat diversity

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

Electromagnetic field in Lyra manifold: a first order approach

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

Resonance and chaos .1. First-order interior resonances

Analytical models for studying the dynamical behaviour of objects near interior, mean motion resonances are reviewed in the context of the planar, circular, restricted three-body problem. The predicted widths of the resonances are compared with the results of numerical integrations using Poincare surfaces of section with a mass ratio of 10(-3) (similar to the Jupiter-Sun case). It is shown that for very low eccentricities the phase space between the 2:1 and 3:2 resonances is predominantly regular, contrary to simple theoretical predictions based on overlapping resonance. A numerical study of the 'evolution' of the stable equilibrium point of the 3:2 resonance as a function of the Jacobi constant shows how apocentric libration at the 2:1 resonance arises; there is evidence of a similar mechanism being responsible for the centre of the 4:3 resonance evolving towards 3:2 apocentric libration. This effect is due to perturbations from other resonances and demonstrates that resonances cannot be considered in isolation. on theoretical grounds the maximum libration width of first-order resonances should increase as the orbit of the perturbing secondary is approached. However, in reality the width decreases due to the chaotic effect of nearby resonances.