1,354,209 research outputs found
Fibring: Completeness Preservation
No full textA completeness theorem is established for logics with congruence endowed with general semantics (in the style of general frames). As a corollary, completeness is shown to be preserved by fibring logics with congruence provided that congruence is retained in the resulting logic.
The class of logics with equivalence is shown to be closed under fibring and to be included in the class of logics with congruence. Thus, completeness is shown to be preserved by fibring logics with equivalence and general semantics.
An example is provided showing that completeness is not always preserved by fibring logics endowed with standard (non general) semantics. A categorial characterization of fibring is provided using coproducts and cocartesian liftings
Truth-values as labels: a general recipe for labelled deduction
No full textWe introduce a general recipe for presenting non-classical logics in a modular and uniform way as labelled deduction systems. Our recipe is based on a labelling mechanism where labels are general entities that are present, in one way or another, in all logics, namely truth-values. More specifically, the main idea underlying our approach is the use of algebras of truth-values, whose operators reflect the semantics we have in mind, as the labelling algebras of our labelled deduction systems. The "truth-values as labels" approach allows us to give generalized systems for multiple-valued logics within the same formalism: since we can take multiple-valued logics as meaning not only finitely or infinitely many-valued logics but also power-set logics, i.e. logics for which the denotation of a formula can be seen as a set of worlds, our recipe allows us to capture also logics such as modal, intuitionistic and relevance logics, thus providing a first step towards the fibring of these logics with many-valued ones
Labelled Deduction over Algebras of Truth-Values
No full textWe introduce a framework for presenting non-classical logics in a modular and uniform way as labelled natural deduction systems. The use of algebras of truth-values as the labelling algebras of our systems allows us to give generalized systems for multiple-valued logics. More specifically, our framework generalizes previous work where labels represent worlds in the underlying Kripke structure: since we can take multiple-valued logics as meaning not only finitely or infinitely many-valued logics but also power-set logics, our framework allows us to present also logics such as modal, intuitionistic and relevance logics, thus providing a first step towards fibring these logics with many-valued ones
Modal Sequent Calculi Labelled with Truth-values: Completeness, Duality and Analyticity
No full textLabelled sequent calculi are provided for a wide class of normal modal systems using truth values as labels. The rules for formula constructors are common to all modal systems. For each modal system, specific rules for truth values are provided that reflect the envisaged properties of the accessibility relation. Both local and global reasoning are supported. Strong completeness is proved for a natural two-sorted algebraic semantics. As a corollary, strong completeness is also obtained over general Kripke semantics. A duality result is established between the category of sober algebras and the category of general Kripke structures. A simple enrichment of the proposed sequent calculi is proved to be complete over standard Kripke structures. The calculi are shown to be analytic in a useful sense
Fibring modal first-order logics: Completeness preservation
No full textFibring is defined as a mechanism for combining logics with a firstorder base, at both the semantic and deductive levels. A completeness theorem is established for a wide class of such logics, using a variation of the Henkin method that takes advantage of the presence of equality and inequality in the logic. As a corollary, completeness is shown to be preserved when fibring logics in that class. A modal first-order logic is obtained as a fibring where neither the Barcan formula nor its converse hold.
Deriving Liveness Goals from Temporal Logic Specifications
No full textIntroduction The use of temporal logic has been widely explored both on the fields of specification and certification of properties of reactive systems (Pnueli, 1977), (Sernadas, 1980), (Fiadeiro and Maibaum, 1992), (Clarke, Grumberg and Kurshan, 1992), (Manna and Pnueli, 1992), (Manna and Pnueli, 1993), (Sernadas, Sernadas and Costa, 1995), (Sernadas, Sernadas and Ramos, 1996) and in monitoring (Hulsmann and Saake, 1991), (Kung, 1984), (Lipeck and Saake, 1987), (Schwiderski, Hartmann and Saake, 1994). The advantages are known to lie on the clear declarative formalization of the system at hand and on the use of temporal verification techniques to prove properties of the specified systems. Temporal logic specification has also given an important contribution towards the establishment of suitable compositional specification frameworks (Barringer, Kuiper and Pnueli, 1984). -- This work was partly supported by CEC under ESPRIT-III BRA WG 6071 IS-CORE (Information
Preservation by fibring of the finite model property
No full textFundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)Capitalizing on the graph-theoretic account of fibring proposed in Sernadas et al.(2009, J. Log. Comput., 19, 1321-1357), we show that fibring preserves the finite model property under mild conditions. Illustrations are provided for modal, deontic, paraconsistent and linear logics.212375402FCTEU FEDER [KLog PTDC/MAT/68723/2006, QSec PTDC/EIA/67661/2006]Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)EU FEDER [KLog PTDC/MAT/68723/2006, QSec PTDC/EIA/67661/2006]FAPESP [2004/14107-2
Nonsequential Automata Semantics for a Concurrent, Ob ject-Based Language
No full textcfl1998 Published by Elsevier Science B. V. Menezes, Sernadas & Costa 1 Introduction We construct a semantic domain with full concurrency which satisfies the diagonal compositionality requirement, i.e., reifications compose (vertically), reflecting the stepwise description of systems, involving several levels of abstraction, and distributes through combinators (horizontally), meaning that the reification of a composite system is the composition of the reification of its parts
Probabilistic Situation Calculus Paulo Mateus a, ∗ António Pacheco b,∗ ∗ Javier Pinto c,∗∗ ∗ Amílcar Sernadas a,∗
No full textIn this article we propose a Probabilistic Situation Calculus logical language to represent and reason with knowledge about dynamic worlds in which actions have uncertain effects. Uncertain effects are modeled by dividing an action into two subparts: a deterministic (agent produced) input and a probabilistic reaction (produced by nature). We assume that the probabilities of the reactions have known distributions. Our logical language is an extension to Situation Calculae in the style proposed by Raymond Reiter. There are three aspects to this work: First, we extend the language in order to accommodate the necessary distinctions (e.g., the separation of actions into inputs and reactions). Second, we develop the notion of Randomly Reactive Automata in order to specify the semantics of our Probabilistic Situa-tion Calculus. Finally, we develop a reasoning system in Mathematica capable of performing temporal projection in the Probabilistic Situation Calculus
Object-Oriented Design of Information Systems: Theoretical Foundations
No full textData Types, M. Bidoit, C. Choppy (eds.), LNCS 655, SpringerVerlag , Berlin 1992, 40-66 [EM85] Ehrig,H.;Mahr,B.: Fundamentals of Algebraic Specification 1. Springer-Verlag, Berlin 1985 [ES91] Ehrich, H.-D.; Sernadas, A.: Fundamental Object Concepts and Constructions. Information Systems -- Correctness and Reusability, Proc. ISCORE Workshop'91 (G. Saake, A. Sernadas, eds.), Informatik-Berichte 91-03, Techn. Univ. Braunschweig 1991, 1-24 [ESS92] Ehrich,H.-D.;Saake,G.;Sernadas,A.: Concepts of Object-Orientation. Proc. 2nd Workshop Informationssysteme und Kunstliche Intelligenz: Modellierung, InformatikFachberichte 303, Springer-Verlag, Berlin 1992, 1-19 [FM92] Fiadeiro, J.; Maibaum, T.: Temporal Theories as Modularisation Units for Concurrent System Specification, Formal Aspects of Computing 4(3), 1992, 239-272 [FSMS92] Fiadeiro,J.;Sernadas,C.;Maibaum,T.;Sernadas,A.: Describing and Structuring Objects for Conceptual Schema Development. Conceptual Modelling, Databases and CASE: An Integrate..
- …
