Fundamenta Informaticae - Volume 106, issue 2-4

Authors: Ono, Hiroakira | Kanazawa, Makoto | de Queiroz, Ruy

Article Type: Other

DOI: 10.3233/FI-2011-379

Citation: Fundamenta Informaticae, vol. 106, no. 2-4, pp. i-ii, 2011

Authors: Alves, Gleifer V. | de Oliveira, Anjolina G. | de Queiroz, Ruy

Article Type: Research Article

Abstract: A normalization procedure is presented for a classical natural deduction (ND) proof system. This proof system, called N-Graphs, has a multiple conclusion proof structure, where cycles are allowed. With this, we have developed a thorough treatment of cycles, including cycles normalization via an algorithm. We also demonstrate the usefulness of the graphical framework of N-Graphs, where derivations are seen as digraphs. We use geometric perspective techniques to establish the normalization mechanism, thus giving a direct normalization proof. Moreover, the subformula and separation properties are determined.

Keywords: proof theory, normalization, proof-graphs, multiple conclusion, cycles

DOI: 10.3233/FI-2011-380

Citation: Fundamenta Informaticae, vol. 106, no. 2-4, pp. 119-147, 2011

Authors: Amato, Gianluca | Scozzari, Francesca

Article Type: Research Article

Abstract: In the theory of abstract interpretation, a domain is complete when abstract computations are as precise as concrete computations. In addition to the standard notion of completeness, we introduce the concept of observational completeness. A domain is observationally complete for an observable π when abstract computations are as precise as concrete computations, if we only look at properties in π. We prove that continuity of state-transition functions ensures the existence of the least observationally complete domain and we provide a constructive characterization. We study the relationship between the least observationally complete domain and the complete shell. We provide sufficient conditions …under which they coincide, and show several examples where they differ, included a detailed analysis of cellular automata. Show more

Keywords: Abstract interpretation, completeness, static analysis, cellular automata

DOI: 10.3233/FI-2011-381

Citation: Fundamenta Informaticae, vol. 106, no. 2-4, pp. 149-173, 2011

Authors: Belardinelli, Francesco | Lomuscio, Alessio

Article Type: Research Article

Abstract: We investigate quantified interpreted systems, a computationally grounded semantics for a first-order temporal epistemic logic on linear time. We report a completeness result for the monodic fragment of a language that includes LTL modalities as well as distributed and common knowledge. We exemplify possible uses of the formalism by analysing message passing systems, a typical framework for distributed systems, in a first-order setting.

Keywords: First-order Modal Logic, Temporal Logic, Epistemic Logic, Multi-Agent Systems, Completeness

DOI: 10.3233/FI-2011-382

Citation: Fundamenta Informaticae, vol. 106, no. 2-4, pp. 175-190, 2011

Authors: Caleiro, Carlos | Gonçalves, Ricardo

Article Type: Research Article

Abstract: Logical matrices are widely accepted as the semantic structures that most naturally fit the traditional approach to algebraic logic. The behavioral approach to the algebraization of logics extends the applicability of the traditional methods of algebraic logic to a wider range of logical systems, possibly encompassing many-sorted languages and non-truth-functional phenomena. However, as one needs to work with behavioral congruences, matrix semantics are unsuited to the behavioral setting. In [5], a promising version of algebraic valuation semantics was proposed in order to fill in this gap. Herein, we define the class of valuations that should be canonically associated to a …logic, and we show, by means of new meaningful bridge results, how it is related to the behaviorally equivalent algebraic semantics of a behaviorally algebraizable logic. Show more

Keywords: algebraic logic, logical matrix, behavioral algebraization, valuation semantics

DOI: 10.3233/FI-2011-383

Citation: Fundamenta Informaticae, vol. 106, no. 2-4, pp. 191-209, 2011

Authors: de Groote, Philippe | Pogodalla, Sylvain | Pollard, Carl

Article Type: Research Article

Abstract: Recent discussions of grammatical architectures have distinguished two competing approaches to the syntax-semantics interface: syntactocentrism, wherein syntactic structures are mapped or transduced to semantics (and phonology), vs. parallelism, wherein semantics (and phonology) communicates with syntax via a nondirectional (or relational) interface. This contrast arises for instance in dealing with in situ operators. The aim of this paper is threefold: first, we show how the essential content of a parallel framework, convergent grammar (CVG), can be encoded within abstract categorial grammar (ACG), a generic framework which has mainly been used, until now, to encode syntactocentric architectures. Second, using such a generic …framework allows us to relate the mathematical characterization of parallelism in CVG with that of syntactocentrism in mainstream categorial grammar (CG), suggesting that the distinction between parallel and syntactocentric formalisms is superficial in nature. More generally, it shows how to provide mildly context sensitive languages (MCSL), which are a clearly defined class of languages in terms of ACG, with a relational syntax-semantics interface. Finally, while most of the studies on the generative power of ACG have been related to formal languages, we show that ACG can illuminate a linguistically motivated framework such as CVG. Show more

Keywords: Grammatical formalism, type theory, linear logic, lambda calculus, mathematics of language, syntax-semantics interface

DOI: 10.3233/FI-2011-384

Citation: Fundamenta Informaticae, vol. 106, no. 2-4, pp. 211-231, 2011

Authors: Link, Sebastian

Article Type: Research Article

Abstract: Database design aims to find a database schema that permits the efficient processing of common types of queries and updates on future database instances. Full first-order hierarchical decompositions constitute a large class of database constraints that can provide assistance to the database designer in identifying a suitable database schema. We establish finite axiomatisations of full first-order hierarchical decompositions that mimic best database design practice. That is, an inference engine derives all the independent collections of the universal schema during database normalization, and the designer determines during database denormalization which re-combinations of these independent collections manifest the final database schema. We …also show that well-known correspondences between multivalued dependencies, degenerated multivalued dependencies, and a fragment of Boolean propositional logic do not extend beyond binary full first-order hierarchical decompositions. Show more

Keywords: Relational model of data, Database decomposition, Database constraint, Axiomatisation, Propositional Logic

DOI: 10.3233/FI-2011-385

Citation: Fundamenta Informaticae, vol. 106, no. 2-4, pp. 233-258, 2011

Authors: Kontinen, Juha | Nurmi, Ville

Article Type: Research Article

Abstract: Team logic is a new logic, introduced by Väänänen [12], extending dependence logic by classical negation. Dependence logic adds to first-order logic atomic formulas expressing functional dependence of variables on each other. It is known that on the level of sentences dependence logic and team logic are equivalent with existential second-order logic and full second-order logic, respectively. In this article we show that, in a sense that we make explicit, team logic and second-order logic are also equivalent with respect to open formulas. A similar earlier result relating open formulas of dependence logic to the negative fragment of existential second-order …logic was proved in [8]. Show more

Keywords: Dependence logic, Team logic, Team

DOI: 10.3233/FI-2011-386

Citation: Fundamenta Informaticae, vol. 106, no. 2-4, pp. 259-272, 2011

Authors: Maruyama, Yoshihiro

Article Type: Research Article

Abstract: Stone-type duality connects logic, algebra, and topology in both conceptual and technical senses. This paper is intended to be a demonstration of this slogan. In this paper we focus on some versions of Fitting's L-valued logic and L-valued modal logic for a finite distributive lattice L. Building upon the theory of natural dualities, which is a universal algebraic theory of categorical dualities, we establish a Jónsson-Tarski-style duality for algebras of L-valued modal logic, which encompasses Jónsson-Tarski duality for modal algebras as the case L = 2. We also discuss how the dualities change when the algebras are enriched by truth …constants. Topological perspectives following from the dualities provide compactness theorems for the logics and the effective classification of categories of algebras involved, which tells us that Stone-type duality makes it possible to use topology for logic and algebra in significant ways. Show more

Keywords: Stone-type duality, the theory of natural dualities, algebraic logic, Fitting's many-valued modal logic, compactness theorem, classification of categories

DOI: 10.3233/FI-2011-387

Citation: Fundamenta Informaticae, vol. 106, no. 2-4, pp. 273-294, 2011

Authors: Nieves, Juan Carlos | Osorio, Mauricio | Zepeda, Claudia

Article Type: Research Article

Abstract: In the literature, there are several approaches which try to perform common sense reasoning. Among them, the approaches which have probably received the most attention the last two decades are the approaches based on logic programming semantics with negation as failure and argumentation theory. Even though both approaches have their own features, it seems that they share some common behaviours which can be studied by considering the close relationship between logic programming semantics and extension-based argumentation semantics. In this paper, we will present a general recursive schema for defining new logic programming semantics. This schema takes as input any basic …logic programming semantics, such as the stable model semantics, and gives as output a new logic programming semantics which satisfies some desired properties such as relevance and the existence of the intended models for every normal program. We will see that these new logic programming semantics can define candidate extension-based argumentation semantics. These new argumentation semantics will overcome some of the weakness of the extension-based argumentation semantics based on admissible sets. In fact, we will see that some of these new argumentation semantics have similar behaviour to the extension-based argumentation semantics built in terms of strongly connected components. Show more

Keywords: Non-monotonic reasoning, extension-based argumentation semantics and logic programming semantics, logic programming

DOI: 10.3233/FI-2011-388

Citation: Fundamenta Informaticae, vol. 106, no. 2-4, pp. 295-319, 2011

Authors: Wang, Ren-June

Article Type: Research Article

Abstract: It is well known that Modal Epistemic logic (MEL) suffers from the problem of logical omniscience. In this paper, we will argue that in order to solve the problem, the temporal dimension of knowledge has to be revealed and following this analysis, we present a general epistemic framework, timed Modal Epistemic Logic (tMEL), modified from MEL, such that the time at which a formula is known by an agent based on his reasoning procedure is explicitly stated. With the help of the additional temporal devices, we are able to determine what is actually known by the agent within a reasonable …time of reasoning. The discussions will focus on tS4, the tMEL counterpart of S4, but the method can be uniformly generalized to the study of other tMEL logics. Both the semantics and axiomatic proof systems will be provided, accompanied by soundness and completeness results, and other technical features of tMEL are also examined. This work originates from the study of Justification Logic, which shapes many aspects of this paper, and is also a direct response to the request to utilize the use of awareness functions such that time can be added to the picture. A generalized awareness function is employed in the semantics to trace when a formula is deduced. Show more

DOI: 10.3233/FI-2011-389

Citation: Fundamenta Informaticae, vol. 106, no. 2-4, pp. 321-338, 2011