#### Electronic Notes in Theoretical Computer Science

Journal Information
ISSN : 1571-0661
Total articles ≅ 6,224
Current Coverage
SCOPUS
COMPENDEX
Archived in
SHERPA/ROMEO
Filter:

#### Latest articles in this journal

Published: 24 November 2020
Electronic Notes in Theoretical Computer Science, Volume 354, pp 141-155; https://doi.org/10.1016/j.entcs.2020.10.011

Abstract:
Logic Programming and fuzzy logic are active areas of research, and their scopes in terms of applications are growing fast. Fuzzy logic is a branch of many-valued logic based on the paradigm of inference under vagueness. In this work we recall some of the interplay between three 3-valued logics that are relevant in these areas: The Lukasiewicz logic, the intermediate logic G3 and the paraconsistent logic ${G}_{3}^{\prime }$, and we present a contribution to the area of answer sets that consists in extending a definition of stable model based on proof theory in logic G3, to a more general definition that can be based on any of the more expressive logics ${G}_{3}^{\prime }$ or Lukasiewicz. Finally we present and explore a new 4-valued logic that bears relation to G3 and to Lukasiewicz 4-valued logic.
Published: 24 November 2020
Electronic Notes in Theoretical Computer Science, Volume 354, pp 61-74; https://doi.org/10.1016/j.entcs.2020.10.006

Abstract:
In 2016 Béziau, introduce a restricted notion of paraconsistency, the so-called genuine paraconsistency. A logic is genuine paraconsistent if it rejects the laws φφψ and ⊢ ¬(φ ∧ ¬φ). In that paper the author analyzes, among the three-valued logics, which of them satisfy this property. If we consider multiple-conclusion consequence relations, the dual properties of those above mentioned are ⊢ φφ and ¬(ψ∨¬ψ) ⊢. We call genuine paracomplete logics those rejecting the mentioned properties. We present here an analysis of the three-valued genuine paracomplete logics.
Published: 24 November 2020
Electronic Notes in Theoretical Computer Science, Volume 354, pp 75-89; https://doi.org/10.1016/j.entcs.2020.10.007

Abstract:
We analyze the vertex-coloring problem restricted to planar graphs and propose to consider classic wheels and polyhedral wheels as basic patterns for the planar graphs. We analyze the colorability of the composition among wheels and introduce a novel algorithm based on three rules for the vertex-coloring problem. These rules are: 1) Selecting vertices in the frontier. 2) Processing subsumed wheels. 3) Processing centers of the remaining wheels. Our method forms a maximal independent set S1V (G) consisting of wheel's centers, and a maximum number of vertices in the frontier of the planar graph. Thus, we show that if the resulting graph G′ = (G − S1) is 3-colorable, then this implies the existence of a valid 4-coloring for G.
Published: 24 November 2020
Electronic Notes in Theoretical Computer Science, Volume 354, pp 17-28; https://doi.org/10.1016/j.entcs.2020.10.003

Abstract:
Murphree's Numerical Term Logic is a logic capable of representing and performing inference with numerical quantifiers by modifying Sommers' Term Functor Logic: in this contribution we offer a tableaux method for it.
Published: 24 November 2020
Electronic Notes in Theoretical Computer Science, Volume 354, pp 3-16; https://doi.org/10.1016/j.entcs.2020.10.002

Abstract:
The Craig Interpolation Theorem is a well-known property in the mathematical logic curricula, with many domain applications, such as in the modularization of formal specifications and ontologies. This property states the following: given an implication, say formula ϕ implies another formula ψ, then there is a formula β, called the interpolant, in the common language of ϕ and ψ, such that ϕ also implies β, as well as β implies ψ. Although it is already known that the propositional multi-modal logic Km enjoys Craig interpolation, we are not aware of method providing an explicit construction of interpolants. We describe in this paper a constructive proof of the Craig interpolation property on the multi-modal logic Km. Interpolants can be explicitly computed from the proof. Furthermore, we also describe an upper bound for the computation of interpolants. The proof is based on the application of Maehara technique on a tree-hypersequent calculus. As a corollary of interpolation, we also show Beth definability and Robinson joint consistency.
Published: 24 November 2020
Electronic Notes in Theoretical Computer Science, Volume 354, pp 107-127; https://doi.org/10.1016/j.entcs.2020.10.009

Abstract:
We present a dual sequent calculus for the necessity fragment of the constructive modal logic S4 and show its adequacy for proof-search in the style of modern interactive theorem provers. The main feature of dual systems is the use of two contexts to capture the notions of true and valid formulas, without using any formal semantics. This attribute allows us to give simple rules for the □ operator that, most of the time, grant the substitution of a strict modal reasoning by a pure propositional one, thus simplifying the proof-search process. Moreover, we introduce a formal notion of backward proof corresponding to a bottom-up construction of a derivation tree by means of a left-to-right depth-first proof-search.
Published: 24 November 2020
Electronic Notes in Theoretical Computer Science, Volume 354, pp 157-170; https://doi.org/10.1016/j.entcs.2020.10.012

Abstract:
We introduce three 5-valued paraconsistent logics that we name FiveASP1, FiveASP2 and FiveASP3. Each of these logics is genuine and paracomplete. The new value is called e attempting to model the notion of ineffability. If one drops e from any of these logics one obtains a well known 4-valued logic introduced by Avron. If, on the other hand one drops the “implication” connective from any of these logics, one obtains Priest logic FDEe. We present some properties of these logics.
Published: 24 November 2020
Electronic Notes in Theoretical Computer Science, Volume 354, pp 171-186; https://doi.org/10.1016/j.entcs.2020.10.013

Abstract:
Dynamic typed languages are characterized by their expressiveness and flexibility to develop prototypes, while static typed languages allow early detection of errors and the optimization of source code. Gradual typing languages allow programmers to make use of both approaches, static and dynamic typing, and thus, obtaining the advantages that both represent. The objective here is to revisit the static part of the approach to a gradual interpretation of union types based on the design of Gradual Union Types through an extension with the record data-structure. This contributes to understand the abstraction and reasoning behind Gradual Typing in order to have useful future extensions for other data-structures.
Published: 24 November 2020
Electronic Notes in Theoretical Computer Science, Volume 354, pp 129-139; https://doi.org/10.1016/j.entcs.2020.10.010

Abstract:
Besides tutoring and consultancies, the development of academic and scientific documents in universities evidenced collaborative work. This paper presents an ontology-based approach to describe different modes of collaboration by reusing and enriching data from an institutional repository, from a collection of posters. The approach uses an application ontology that makes explicit the relationships among authors and posters. The paper presents a list of competency questions that are answered in natural language and by the ontology terminology. The proposed approach is of value as this offers machine-readable data to support further analysis and inference mechanisms. This paper represents a reviewed version of the described for the CEUR proceedings for the “Twelfth Latin American Workshop on New Methods of Reasoning 2019 Logic / Languages, Algorithms, New Methods of Reasoning (LANMR 2019)”.
Published: 24 November 2020
Electronic Notes in Theoretical Computer Science, Volume 354, pp 91-105; https://doi.org/10.1016/j.entcs.2020.10.008

Abstract:
We present an algorithm for the coloring of planar graphs based on the construction of a maximal independent set S of the input graph. The maximal independent set S must fulfill certain characteristics. For example, S contains the vertex that appears in a maximum number of odd cycles of G. The construction of S considers the internal-face graph of the input graph G in order to select each vertex belonging to a maximal number of odd faces of G.