Every Finitely Reducible Logic has the Finite Model Property with Respect to the Class of ♦-Formulae

In this paper a unified framework for dealing with a broad family of propositional multimodal logics is developed. The key tools for presentation of the logics are the notions of closure relation operation and monotonous relation operation. The two classes of logics: FiRe-logics (finitely reducible logics) and LaFiRe-logics (FiRe-logics with local agreement of accessibility relations) are introduced within the proposed framework. Further classes of logics can be handled indirectly by means of suitable translations. It is shown that the logics from these classes have the finite model property with respect to the class of -formulae, i.e. each -formula has a -model iff it has a finite -model. Roughly speaking, a -formula is logically equivalent to a formula in negative normal form without occurrences of modal operators with necessity force. In the proof we introduce a substantial modification of Claudio Cerrato's filtration technique that has been originally designed for graded modal logics. The main core of the proof consists in building adequate restrictions of models while preserving the semantics of the operators used to build terms indexing the modal operators.     

Bounded contraction and Gentzen-style formulation of Łukasiewicz logics

In this paper, we consider multiplicative-additive fragments of affine propositional classical linear logic extended with n-contraction. To be specific, n-contraction (n 2) is a version of the contraction rule where (n+ 1) occurrences of a formula may be contracted to n occurrences. We show that expansions of the linear models for (n + 1)- valued ukasiewicz logic are models for the multiplicative-additive classical linear logic, its affine version and their extensions with n-contraction. We prove the finite axiomatizability for the classes of finite models, as well as for the class of infinite linear models based on the set of rational numbers in the interval [0, 1]. The axiomatizations obtained in a Gentzen-style formulation are equivalent to finite and infinite-valued ukasiewicz logics.Presented by Jan Zygmunt     

The finite model property for BCI and related systems

We prove the finite model property (fmp) for BCI and BCI with additive conjunction, which answers some open questions in Meyer and Ono [11]. We also obtain similar results for some restricted versions of these systems in the style of the Lambek calculus [10, 3]. The key tool is the method of barriers which was earlier introduced by the author to prove fmp for the product-free Lambek calculus [2] and the commutative product-free Lambek calculus [4].Presented by H. Ono     

Statistical inference based on latent ability estimates

The quality of approximations to first and second order moments (e.g., statistics like means, variances, regression coefficients) based on latent ability estimates is being discussed. The ability estimates are obtained using either the Rasch, or the two-parameter logistic model. Straightforward use of such statistics to make inferences with respect to true latent ability is not recommended, unless we account for the fact that the basic quantities are estimates. In this paper true score theory is used to account for the latter; the counterpart of observed/true score being estimated/true latent ability. It is shown that statistics based on the true score theory are virtually unbiased if the number of items presented to each examinee is larger than fifteen. Three types of estimators are compared: maximum likelihood, weighted maximum likelihood, and Bayes modal. Furthermore, the (dis)advantages of the true score method and direct modeling of latent ability is discussed.     

Agent deliberation in an executable temporal framework

Autonomous agents are not so difficult to construct. Constructing autonomous agents that will work as required is much harder. A clear way in which we can design and analyse autonomous systems so that we can be more confident that their behaviour is as required is to use formal methods. These can, in principle, allow us to exactly specify the behaviour of the agent, and verify that any implementation has the properties required. In addition to using a more formal approach, it is clear that problems of conceptualisation and analysis can be aided by the use of an appropriate abstraction.In this article we tackle one particular aspect of formal methods for agent-based systems, namely the formal representation and implementation of deliberation within agents. The key aspect here is simplicity. Agents are specified using a relatively simple temporal logic and are executed by directly interpreting such temporal formulae. Deliberation is captured by modifying the way in which execution handles its temporal goals. Thus, in this article we provide motivations, theoretical underpinnings, implementation details, correctness arguments, and comparisons with related work.     

Completeness and Decidability Results for Some Propositional Modal Logics Containing “Actually” Operators

The addition of actually operators to modal languages allows us to capture important inferential behaviours which cannot be adequately captured in logics formulated in simpler languages. Previous work on modal logics containing actually operators has concentrated entirely upon extensions of KT5 and has employed a particular model-theoretic treatment of them. This paper proves completeness and decidability results for a range of normal and nonnormal but quasi-normal propositional modal logics containing actually operators, the weakest of which are conservative extensions of K, using a novel generalisation of the standard semantics.     

FINITE MODELS CONSTRUCTED FROM CANONICAL FORMULAS

This paper obtains the weak completeness and decidability results for standard systems of modal logic using models built from formulas themselves. This line of work began with Fine (Notre Dame J. Form. Log. 16:229–237, 1975). There are two ways in which our work advances on that paper: First, the definition of our models is mainly based on the relation Kozen and Parikh used in their proof of the completeness of PDL, see (Theor. Comp. Sci. 113–118, 1981). The point is to develop a general model-construction method based on this definition. We do this and thereby obtain the completeness of most of the standard modal systems, and in addition apply the method to some other systems of interest. None of the results use filtration, but in our final section we explore the connection.     

On Dynamic Topological and Metric Logics

We investigate computational properties of propositional logics for dynamical systems. First, we consider logics for dynamic topological systems (W.f), fi, where W is a topological space and f a homeomorphism on W. The logics come with ‘modal’ operators interpreted by the topological closure and interior, and temporal operators interpreted along the orbits {w, f(w), f² (w), ˙˙˙} of points w ε W. We show that for various classes of topological spaces the resulting logics are not recursively enumerable (and so not recursively axiomatisable). This gives a ‘negative’ solution to a conjecture of Kremer and Mints. Second, we consider logics for dynamical systems (W, f), where W is a metric space and f and isometric function. The operators for topological interior/closure are replaced by distance operators of the form ‘everywhere/somewhere in the ball of radius a, ‘for a ε Q ⁺. In contrast to the topological case, the resulting logic turns out to be decidable, but not in time bounded by any elementary function.     

The Classification of Propositional Calculi

We discuss Smirnovs problem of finding a common background for classifying implicational logics. We formulate and solve the problem of extending, in an appropriate way, an implicational fragment H of the intuitionistic propositional logic to an implicational fragment TV of the classical propositional logic. As a result we obtain logical constructions having the form of Boolean lattices whose elements are implicational logics. In this way, whole classes of new logics can be obtained. We also consider the transition from implicational logics to full logics. On the base of the lattices constructed, we formulate the main classification principles for propositional logics.