Subscribe: Journal of Logic and Computation - current issue
Preview: Journal of Logic and Computation - current issue

Journal of Logic and Computation Current Issue

Published: Thu, 24 Aug 2017 00:00:00 GMT

Last Build Date: Wed, 30 Aug 2017 04:48:48 GMT


Universal logic and computation


This special issue contains papers related to Universal Logic and Computation. The work on this special issue started about three years ago with the intention to dedicate it to Jean-Yves Béziau on the occasion of his 50th anniversary which actually took place a couple of years ago in the middle of the process of preparing this special issue. I think even now it is not too late to dedicate it to Jean-Yves, who has been and still is a main promoter of this quite revolutionary new trend in logic, known as Universal Logic. He has done this especially by building from scratch a quite amazing academic infrastructure in support of Universal Logic. This includes a dedicated World Congress and School (until now there have been five such events), a book series (Studies in Universal Logic, Springer Basel) and a journal (Logica Universalis, Springer Basel).

Paraconsistency in hybrid logic


As in standard knowledge bases, hybrid knowledge bases (i.e. sets of information specified by hybrid formulas) may contain inconsistencies arising from different sources, namely from the many mechanisms used to collect relevant information. Being a fact, rather than a queer anomaly, inconsistency also needs to be addressed in the context of hybrid logic applications. This article introduces a paraconsistent version of hybrid logic which is able to accommodate inconsistencies at local points without implying global failure. A main feature of the resulting logic, crucial to our approach, is the fact that every hybrid formula has an equivalent formula in negation normal form. The article also provides a measure to quantify the inconsistency of a hybrid knowledge base, useful as a possible basis for comparing knowledge bases. Finally, the concepts of extrinsic and intrinsic inconsistency of a theory are discussed.

An institutional approach to positive coalgebraic logic


Positive modal logic, as introduced by Dunn in 1995, is the negation-free fragment of the standard modal logic of all Kripke frames. Positive coalgebraic logic, introduced by the authors in a previous work, expands the above result from Kripke frames to more general transition systems, namely to coalgebras of weak-pullback preserving functors. We show that this construction is both modular and uniform in the functor giving the type of coalgebra. More precisely, we formalize both Set and Pos-based coalgebraic modal logic as institutions, and we exhibit a morphism of institutions between them giving the positive fragment of coalgebraic modal logic.

Polynomial ring calculus for modalities


This article investigates new algebraic proof methods for the modal logics K, KD, T, S4, S5 and for intuitionistic logic. The methods are based on the Polynomial Ring Calculus introduced in [6], and extend the results obtained in [1]. Several examples are provided, as well as a comparison with other methods.

From conventional to institution-independent logic programming


We propose a logic-independent approach to logic programming through which the paradigm as we know it for Horn-clause logic can be explored for other formalisms. Our investigation is based on abstractions of notions such as logic program, clause, query, solution and computed answer, which we develop over Goguen and Burstall's theory of institutions. These give rise to a series of concepts that formalize the interplay between the denotational and the operational semantics of logic programming. We examine properties concerning the satisfaction of quantified sentences, discuss a variant of Herbrand's theorem that is not limited in scope to any particular logical system or construction of logic programs, and describe a general resolution-based procedure for computing solutions to queries. We prove that this procedure is sound; moreover, under additional hypotheses that reflect faithfully properties of actual logic-programming languages, we show that it is also complete.

Downward Löwenheim–Skolem Theorem and interpolation in logics with constructors


The present article describes a method for proving Downward Löwenheim–Skolem Theorem within an arbitrary institution satisfying certain logic properties. In order to demonstrate the applicability of the present approach, the abstract results are instantiated to many-sorted first-order logic and preorder algebra. In addition to the first technique for proving Downward Löwenheim–Skolem Theorem, another one is developed, in the spirit of institution-independent model theory, which consists of borrowing the result from a simpler institution across an institution comorphism. As a result, the Downward Löwenheim–Skolem Property is exported from first-order logic to partial algebras, and from higher-order logic with intensional Henkin semantics to higher-order logic with extensional Henkin semantics. The second method successfully extends the domain of application of Downward Löwenheim–Skolem Theorem to other non-conventional logical systems for which the first technique may fail. One major application of Downward Löwenheim–Skolem Theorem is interpolation in constructor-based logics with universally quantified sentences. The interpolation property is established by borrowing it from a base institution for its constructor-based variant across an institution morphism. This result is important as interpolation for constructor-based first-order logics is still an open problem.

How to identify, translate and combine logics?


We give general definitions of logical frameworks and logics. Examples include the logical frameworks LF and Isabelle and the logics represented in them. We apply this to give general definitions for equivalence of logics, translation between logics and combination of logics. We also establish general criteria for the soundness and completeness of these. Our key messages are that the syntax and proof systems of logics are theories; that both semantics and translations are theory morphisms; and that combinations are colimits. Our approach is based on the Mmt language, which lets us combine formalist declarative representations (and thus the associated tool support) with abstract categorical conceptualizations.