106 (1) 2011
- 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.
- 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.
- 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
- 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"
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.
- 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
- Logic, Language, Information and Computation. Preface i-ii
- 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.
- 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.
- 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.
- 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 , 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.
- 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.
- 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.
- Team Logic and Second-Order Logic
Juha Kontinen, Ville Nurmi 259-272
Team logic is a new logic, introduced by Väänänen , 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 .
- 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.
- 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
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.
- 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.