106 (1) 2011

  1. A Paraconsistent Linear-time Temporal Logic
    Norihiro Kamide,  Heinrich Wansing 1-23
    Inconsistency-tolerant reasoning and paraconsistent logic are of growing importance not only in Knowledge Representation, AI and other areas of Computer Science, but also in Philosophical Logic. In this paper, a new logic, paraconsistent linear-time temporal logic (PLTL), is obtained semantically from the linear-time temporal logic LTL by adding a paraconsistent negation. Some theorems for embedding PLTL into LTL are proved, and PLTL is shown to be decidable. A Gentzen-type sequent calculus PLTw for PLTL is introduced, and the completeness and cut-elimination theorems for this calculus are proved. In addition, a display calculus dPLTw for PLTL is defined.
  2. Level Mapping Induced Loop Formulas for Weight Constraint and Aggregate Logic Programs
    Guohua Liu and Jia-Huai You 25-43
    Level mapping and loop formulas are two different means to justify and characterize answer sets for normal logic programs. Both of them specify conditions under which a supported model is an answer set. Though serving a similar purpose, in the past the two have been studied largely in isolation with each other. In this paper, we study level mapping and loop formulas for weight constraint and aggregate (logic) programs. We show that, for these classes of programs, loop formulas can be devised from level mapping characterizations. First, we formulate a level mapping characterization of stable models and show that it leads to a new formulation of loop formulas for arbitrary weight constraint programs, without using any new atoms. This extends a previous result on loop formulas for weight constraint programs, where weight constraints contain only positive literals. Second, since aggregate programs are closely related to weight constraint programs, we further use level mapping to characterize the underlying answer set semantics based on which we formulate loop formulas for aggregate programs. The main result is that for aggregate programs not involving the inequality comparison operator, the dependency graphs can be built in polynomial time. This compares to the previously known exponential time method.
  3. Unsupervised and Supervised Learning Approaches Together for Microarray Analysis
    Indrajit Saha, Ujjwal Maulik,  Sanghamitra Bandyopadhyay,  Dariusz Plewczynski 45-73
    In this article, a novel concept is introduced by using both unsupervised and supervised learning. For unsupervised learning, the problem of fuzzy clustering in microarray data as a multiobjective optimization is used, which simultaneously optimizes two internal fuzzy cluster validity indices to yield a set of Pareto-optimal clustering solutions. In this regards, a new multiobjective differential evolution based fuzzy clustering technique has been proposed. Subsequently, for supervised learning, a fuzzy majority voting scheme along with support vector machine is used to integrate the clustering information from all the solutions in the resultant Pareto-optimal set. The performances of the proposed clustering techniques have been demonstrated on five publicly available benchmark microarray data sets. A detail comparison has been carried out with multiobjective genetic algorithm based fuzzy clustering, multiobjective differential evolution based fuzzy clustering, single objective versions of differential evolution and genetic algorithm based fuzzy clustering as well as well known fuzzy c-means algorithm. While using support vector machine, comparative studies of the use of four different kernel functions are also reported. Statistical significance test has been done to establish the statistical superiority of the proposed multiobjective clustering approach. Finally, biological significance test has been carried out using a web based gene annotation tool to show that the proposed integrated technique is able to produce biologically relevant clusters of co-expressed genes.
    Supplementary Website: The pre-processed and normalized data sets, the matlab code and other related materials are available at http://bio.icm.edu.pl/~darman/moidefc-svm/
  4. Structural Feature-Based Image Hashing and Similarity Metric for Tampering Detection
    Zhenjun Tang,  Shuozhong Wang,  Xinpeng Zhang,  Weimin Wei 75-91
    Structural image features are exploited to construct perceptual image hashes in this work. The image is first preprocessed and divided into overlapped blocks. Correlation between each image block and a reference pattern is calculated. The intermediate hash is obtained from the correlation coefficients. These coefficients are finally mapped to the interval [0, 100], and scrambled to generate the hash sequence. A key component of the hashing method is a specially defined similarity metric to measure the "distance" between hashes. This similarity metric is sensitive to visually unacceptable alterations in small regions of the image, enabling the detection of small area tampering in the image. The hash is robust against content-preserving processing such as JPEG compression, moderate noise contamination, watermark embedding, re-scaling, brightness and contrast adjustment, and low-pass filtering. It has very low collision probability. Experiments are conducted to show performance of the proposed method.
  5. Application of the Method of Editing and Condensing in the Process of Global Decision-making
    Alicja Wakulicz-Deja,  Małgorzata Przybyła-Kasperek 93-117
    The paper presents the process of taking global decisions on the basis of the knowledge of local decision systems, in which sets of conditional attributes are different but not necessarily disjoint. We propose the organization of local decision systems into a multi-agent system with a hierarchical structure. The structure of multi-agent systems and the theoretical aspects of the organization of the system are presented. An editing and a condensing algorithm have been used in the process of global decision making. Also a density-based algorithm has been used in the process of taking global decisions to resolve conflicts. Furthermore, the paper presents the results of experiments conducted using some data sets from UCI repository.

106 (2-4) 2011

  1. Logic, Language, Information and Computation.  Preface i-ii
  2. Proof-graphs: a Thorough Cycle Treatment, Normalization and Subformula Property
    Gleifer V. Alves,  Anjolina G. de Oliveira,  Ruy de Queiroz 119-147
    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.
  3. Observational Completeness on Abstract Interpretation
    Gianluca Amato,  and Francesca Scozzari 149-173
    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 p when abstract computations are as precise as concrete computations, if we only look at properties in p. 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.
  4. First-Order Linear-time Epistemic Logic with Group Knowledge: An Axiomatisation of the Monodic Fragment
    Francesco Belardinelli,  Alessio Lomuscio 175-190
    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.
  5. Towards a Behavioral Algebraic Theory of Logical Valuations
    Carlos Caleiro,  Ricardo Gonçalves 191-209
    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.
  6. About Parallel and Syntactocentric Formalisms: A Perspective from the Encoding of Convergent Grammar into Abstract Categorial Grammar
    Philippe de Groote,  Sylvain Pogodalla,  Carl Pollard 211-231
    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.
  7. On Inferences of Full First-Order Hierarchical Decompositions
    Sebastian Link 233-258
    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 de-normalization 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.
  8. Team Logic and Second-Order Logic
    Juha Kontinen,  Ville Nurmi 259-272
    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].
  9. Dualities for Algebras of Fitting's Many-Valued Modal Logics
    Yoshihiro Maruyama 273-294
    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.
  10. A Schema for Generating Relevant Logic Programming Semantics and its Applications in Argumentation Theory
    Juan Carlos Nieves,  Mauricio Osorio,  Claudia Zepeda 295-319
    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.
  11. Knowledge, Time, and the Problem of Logical Omniscience
    Ren-June Wang 321-338
    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.