Catálogo de publicaciones - libros

We apply the logic-based declarative programming approach of Model Expansion (MX) to a phylogenetic inference task. We axiomatize the task in multi-sorted first-order logic with cardinality constraints. Using the model expansion solver MXG and SAT+cardinality solver MXC, we compare the performance of several MX axiomatizations on a challenging set of test instances. Our methods perform orders of magnitude faster than previously reported declarative solutions. Our best solution involves polynomial-time pre-processing, redundant axioms, and symmetry-breaking axioms. We also discuss our method of test instance generation, and the role of pre-processing in declarative programming.

The model checking problem for open systems (called ) has been intensively studied in the literature, both for finite–state and infinite–state systems. In this paper, we focus on pushdown module checking with respect to –calculus enriched with graded and nominals (). We show that this problem is decidable and solvable in double–exponential time in the size of the formula and in exponential time in the size of the system. This result is obtained by exploiting a classical automata–theoretic approach via . In particular, we reduce in exponential time our problem to the emptiness problem for these automata, which is known to be decidable in . As a key step of our algorithm, we show an exponential improvement of the construction of a nondeterministic parity tree automaton accepting all models of a formula of the considered logic. This result, not only allows our algorithm to match the known lower bound, but it is also interesting by itself, since it allows investigating decision problems related to enriched -calculus formulas in a greatly simplified manner. We conclude the paper with a discussion on the model checking w.r.t. -calculus formulas enriched with backward modalities as well.

We introduce an original 2-valued semantics for Normal Logic Programs (NLPs) extending the well-known Argumentation work of Phan Minh Dung on Admissible Arguments and Preferred Extensions. In the 2-valued Approved Models Semantics set forth, an Approved Model (AM) correspond to the minimal positive strict consistent 2-valued completion of a Dung Preferred Extension. The AMs Semantics enjoys several non-trivial useful properties such as (1) Existence of a 2-valued Model for every NLP; (2) Relevancy, and (3) Cumulativity. Crucially, we show that the AMs Semantics is a conservative extension to the Stable Models (SMs) Semantics in the sense that every SM of a NLP is also an AM, thus providing every NLP with a model: a property not enjoyed by SMs. Integrity constraints, written in a simpler way, are introduced to identify undesired semantic scenarios, whilst permitting these to be produced nevertheless. We end the paper with some conclusions and mention of future work.

Permutative logic (PL) is a noncommutative variant of multiplicative linear logic (MLL) arising from recent investigations concerning the topology of linear proofs. Permutative sequents are structured as oriented surfaces with boundary whose topological complexity is able to encode some information about the exchange in sequential proofs. In this paper we provide a complete permutative sequent calculus by extending that one of PL with rules for additives and exponentials. This extended system, here called (PLL), is shown to be a conservative extension of linear logic and able to enjoy cut-elimination. Moreover, some basic isomorphisms are pointed out.

We present algorithms for the propositional model counting problem #SAT. The algorithms are based on tree-decompositions of graphs associated with the given CNF formula, in particular primal, dual, and incidence graphs. We describe the algorithms in a coherent fashion that admits a direct comparison of their algorithmic advantages. We analyze and discuss several aspects of the algorithms including worst-case time and space requirements and simplicity of implementation. The algorithms are described in sufficient detail for making an implementation reasonably easy.

Given a set of modal formulas of the form (, ), where occurs positively in , the language is obtained by adding to the language of polymodal logic connectives , . Each term is meant to be interpreted as the parametrized least fixed point of the functional interpretation of the term (). Given such a , we construct an axiom system which is sound and complete w.r.t. the concrete interpretation of the language on Kripke frames. If is finite, then is a finite set of axioms and inference rules.

Current Answer Set Programming systems are built on non-monotonic logic programs without function symbols; as well-known, they lead to high undecidability in general. However, function symbols are highly desirable for various applications, which challenges to find meaningful and decidable fragments of this setting. We present the class of logic programs which allows for function symbols, disjunction, non-monotonic negation under answer set semantics, and constraints, while still retaining the decidability of the standard reasoning tasks. Thanks to these features, they are a powerful formalism for rule-based modeling of applications with potentially infinite processes and objects, which allows also for common-sense reasoning. We show that consistency checking and brave reasoning are -complete in general, but have lower complexity for restricted fragments, and outline worst-case optimal reasoning procedures for these tasks. Furthermore, we present a finite representation of the possibly infinitely many infinite stable models of an program, which may be exploited for knowledge compilation purposes.

We consider the temporal logic with since and until modalities. This temporal logic is expressively equivalent over the class of ordinals to first-order logic thanks to Kamp’s theorem. We show that it has a -complete satisfiability problem over the class of ordinals. Among the consequences of our proof, we show that given the code of some countable ordinal ordinal and a formula, we can decide in whether the formula has a model over ordinal . In order to show these results, we introduce a class of simple ordinal automata, as expressive as Büchi ordinal automata. The upper bound for the satisfiability problem of the temporal logic is obtained through a reduction to the nonemptiness problem for the simple ordinal automata.

Mizar is a proof assistant used for formalization and mechanical verification of mathematics. The main use of Mizar is in the development of the Mizar Mathematical Library (MML), in which proofs are verified by the Mizar proof checker. The Mizar proof checker has a quite complex implementation, and also lacks the ability to print out detailed atomic proof steps in a format that is easy to verify by an independent proof-checking tool. This can raise concerns about the correctness of the MML. This paper describes how a Mizar-to-ATP translation (the MPTP system), ATP verification tools (the GDV system), and Automated Theorem Proving (ATP) systems, have been used for an independent cross-verification of a part of the MML.