Search

Your search keyword '"Logic in computer science"' showing total 23 results
Start Over Descriptor "Logic in computer science" Publisher hal ccsd
23 results on '"Logic in computer science"'

1. On the expressive power of non-deterministic and unambiguous Petri nets over infinite words

Author

Olivier Finkel, Michał Skrzypczak, Institut de Mathématiques de Jussieu - Paris Rive Gauche (IMJ-PRG), Université Pierre et Marie Curie - Paris 6 (UPMC)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warsaw, Poland., Institute of Informatics, and Université de Varsovie-Université de Varsovie

Subjects
FOS: Computer and information sciences, Logic in computer science, Algebra and Number Theory, TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, Formal Languages and Automata Theory (cs.FL), TheoryofComputation_GENERAL, Computer Science - Formal Languages and Automata Theory, Petri nets, Highly undecidable properties, Infinite words, Theoretical Computer Science, Borel hierarchy, Wadge degrees, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], Computational Theory and Mathematics, Unambiguous Petri nets, Computer Science::Logic in Computer Science, Cantor topology, Automata and formal languages, Computer Science::Formal Languages and Automata Theory, Information Systems
Abstract

We prove that $\omega$-languages of (non-deterministic) Petri nets and $\omega$-languages of (non-deterministic) Turing machines have the same topological complexity: the Borel and Wadge hierarchies of the class of $\omega$-languages of (non-deterministic) Petri nets are equal to the Borel and Wadge hierarchies of the class of $\omega$-languages of (non-deterministic) Turing machines. We also show that it is highly undecidable to determine the topological complexity of a Petri net $\omega$-language. Moreover, we infer from the proofs of the above results that the equivalence and the inclusion problems for $\omega$-languages of Petri nets are $\Pi_2^1$-complete, hence also highly undecidable. Additionally, we show that the situation is quite the opposite when considering unambiguous Petri nets, which have the semantic property that at most one accepting run exists on every input. We provide a procedure of determinising them into deterministic Muller counter machines with counter copying. As a consequence, we entail that the $\omega$-languages recognisable by unambiguous Petri nets are $\Delta^0_3$ sets., Comment: arXiv admin note: substantial text overlap with arXiv:1712.07945

Published
2021

2. Reconstructing veriT Proofs in Isabelle/HOL

Author

Hans-Jörg Schurr, Mathias Fleury, Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Proof-oriented development of computer-based systems (MOSEL), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Logic in computer science, Computer science, HOL, 02 engineering and technology, computer.software_genre, Mathematical proof, lcsh:QA75.5-76.95, Satisfiability modulo theories, 0202 electrical engineering, electronic engineering, information engineering, Reconstruction procedure, Programming language, lcsh:Mathematics, Proof assistant, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Solver, lcsh:QA1-939, Logic in Computer Science (cs.LO), Trustworthiness, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, 020201 artificial intelligence & image processing, lcsh:Electronic computers. Computer science, computer
Abstract

Automated theorem provers are now commonly used within interactive theorem provers to discharge an increasingly large number of proof obligations. To maintain the trustworthiness of a proof, the automatically found proof must be verified inside the proof assistant. We present here a reconstruction procedure in the proof assistant Isabelle/HOL for proofs generated by the satisfiability modulo theories solver veriT which is part of the smt tactic. We describe in detail the architecture of our improved reconstruction method and the challenges we faced in designing it. Our experiments show that the veriT-powered smt tactic is regularly suggested by Sledgehammer as the fastest method to automatically solve proof goals., Comment: In Proceedings PxTP 2019, arXiv:1908.08639

Published
2019
Full Text
View/download PDF

3. Incompleteness Theorems, Large Cardinals, and Automata over Finite Words

Author

Olivier Finkel, Institut de Mathématiques de Jussieu - Paris Rive Gauche (IMJ-PRG), Université Pierre et Marie Curie - Paris 6 (UPMC)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Gopal T., Jäger G., Steila S., and Finkel, Olivier

Subjects
finite words, Nested word, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Logic in computer science, 02 engineering and technology, 0102 computer and information sciences, ω-automaton, Gödel's incompleteness theorems, 01 natural sciences, Combinatorics, Set (abstract data type), Integer, Peano axioms, 0202 electrical engineering, electronic engineering, information engineering, Computer Science (miscellaneous), Post Correspondence Problem, Quantum finite automata, logic in computer science, context-free grammars, Nondeterministic finite automaton, Automata and formal languages, 0101 mathematics, 2-tape automaton, Mathematics, 060201 languages & linguistics, Discrete mathematics, finitely generated matrix subsemigroups of Z^{3×3}, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Computer Science::Computation and Language (Computational Linguistics and Natural Language and Speech Processing), 06 humanities and the arts, Construct (python library), Context-free grammar, 16. Peace & justice, Automaton, weighted automaton, Post correspondence problem, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], Deterministic finite automaton, finitely generated matrix subsemigroups of Z¨{3×3}, 010201 computation theory & mathematics, 0602 languages and literature, Automata theory, [MATH.MATH-LO] Mathematics [math]/Logic [math.LO], 020201 artificial intelligence & image processing, Computer Science::Formal Languages and Automata Theory
Abstract

We prove that one can construct various kinds of automata over finite words for which some elementary properties are actually independent from strong set theories like [Formula: see text] [Formula: see text] “There exist (at least) [Formula: see text] inaccessible cardinals”, for integers [Formula: see text]. In particular, we prove independence results for languages of finite words generated by context-free grammars, or accepted by 2-tape or 1-counter automata. Moreover we get some independence results for weighted automata and for some related finitely generated subsemigroups of the set [Formula: see text] of 3-3 matrices with integer entries. Some of these latter results are independence results from the Peano axiomatic system PA.

Published
2019
Full Text
View/download PDF

4. Hierarchic Superposition Revisited

Author

Uwe Waldmann, Peter Baumgartner, Data61 [Canberra] (CSIRO), Australian National University (ANU)-Commonwealth Scientific and Industrial Research Organisation [Canberra] (CSIRO), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Carsten Lutz and Uli Sattler and Cesare Tinelli and Anni-Yasmin Turhan and Frank Wolter, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Logic in computer science, Computer science, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Abstraction (mathematics), Algebra, Automated theorem proving, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Fragment (logic), 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Completeness (logic), Computer Science::Logic in Computer Science, Superposition calculus, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Special case, Integer (computer science)
Abstract

International audience; Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arithmetic. A major unsolved research challenge is to design theorem provers that are "reasonably complete" even in the presence of free function symbols ranging into a background theory sort. The hierarchic superposition calculus of Bachmair, Ganzinger, and Waldmann already supports such symbols, but, as we demonstrate, not optimally. This paper aims to rectify the situation by introducing a novel form of clause abstraction, a core component in the hierarchic superposition calculus for transforming clauses into a form needed for internal operation. We argue for the benefits of the resulting calculus and provide two new completeness results: one for the fragment where all background-sorted terms are ground and another one for a special case of linear (integer or rational) arithmetic as a background theory.

Published
2019
Full Text
View/download PDF

5. Wadge Degrees of $\omega$-Languages of Petri Nets

Author

Finkel, Olivier, Institut de Mathématiques de Jussieu - Paris Rive Gauche (IMJ-PRG), and Université Pierre et Marie Curie - Paris 6 (UPMC)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Computer Science - Logic in Computer Science, TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, infinite words, [INFO.INFO-GT]Computer Science [cs]/Computer Science and Game Theory [cs.GT], TheoryofComputation_GENERAL, Mathematics::General Topology, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Petri nets, Mathematics - Logic, Wadge hierarchy, Borel hierarchy, Wadge degrees, Mathematics::Logic, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], Cantor topology, logic in computer science, Automata and formal languages
Abstract

We prove that $\omega$-languages of (non-deterministic) Petri nets and $\omega$-languages of (non-deterministic) Turing machines have the same topological complexity: the Borel and Wadge hierarchies of the class of $\omega$-languages of (non-deterministic) Petri nets are equal to the Borel and Wadge hierarchies of the class of $\omega$-languages of (non-deterministic) Turing machines which also form the class of effective analytic sets. In particular, for each non-null recursive ordinal $\alpha < \omega\_1^{{\rm CK}} $ there exist some ${\bf \Sigma}^0\_\alpha$-complete and some ${\bf \Pi}^0\_\alpha$-complete $\omega$-languages of Petri nets, and the supremum of the set of Borel ranks of $\omega$-languages of Petri nets is the ordinal $\gamma\_2^1$, which is strictly greater than the first non-recursive ordinal $\omega\_1^{{\rm CK}}$. We also prove that there are some ${\bf \Sigma}\_1^1$-complete, hence non-Borel, $\omega$-languages of Petri nets, and that it is consistent with ZFC that there exist some $\omega$-languages of Petri nets which are neither Borel nor ${\bf \Sigma}\_1^1$-complete. This answers the question of the topological complexity of $\omega$-languages of (non-deterministic) Petri nets which was left open in [DFR14,FS14]., Comment: arXiv admin note: text overlap with arXiv:0712.1359, arXiv:0804.3266

Published
2018

6. The Bernays–Schönfinkel–Ramsey Fragment with Bounded Difference Constraints over the Reals Is Decidable

Author

Marco Voigt, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Max-Planck-Gesellschaft, Clare Dixon and Marcelo Finger, Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), and Max-Planck-Gesellschaft-Max-Planck-Gesellschaft

Subjects
Discrete mathematics, Logic in computer science, difference constraints, Bernays–Schönfinkel–Ramsey fragment, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], linear arithmetic constraints, 0102 computer and information sciences, 02 engineering and technology, Predicate (mathematical logic), Arity, 01 natural sciences, Satisfiability, Decidability, Undecidable problem, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, Bounded function, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Computer Science::Programming Languages, 020201 artificial intelligence & image processing, combination of theories, Boolean satisfiability problem, Mathematics
Abstract

First-order linear real arithmetic enriched with uninterpreted predicate symbols yields an interesting modeling language. However, satisfiability of such formulas is undecidable, even if we restrict the uninterpreted predicate symbols to arity one. In order to find decidable fragments of this language, it is necessary to restrict the expressiveness of the arithmetic part. One possible path is to confine arithmetic expressions to difference constraints of the form \(x - y \mathrel {\triangleleft }c\), where \(\mathrel {\triangleleft }\) ranges over the standard relations \( \) and x, y are universally quantified. However, it is known that combining difference constraints with uninterpreted predicate symbols yields an undecidable satisfiability problem again. In this paper, it is shown that satisfiability becomes decidable if we in addition bound the ranges of universally quantified variables. As bounded intervals over the reals still comprise infinitely many values, a trivial instantiation procedure is not sufficient to solve the problem.

Published
2017
Full Text
View/download PDF

7. On the Combination of the Bernays–Schönfinkel–Ramsey Fragment with Simple Linear Integer Arithmetic

Author

Marco Voigt, Christoph Weidenbach, Matthias Horbach, Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Saarland University [Saarbrücken], Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Leonardo de Moura, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Discrete mathematics, Predicate logic, Logic in computer science, Bernays-Schönfinkel-Ramsey fragment, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, 02 engineering and technology, 16. Peace & justice, Data structure, 01 natural sciences, Decidability, Undecidable problem, Complete instantiation, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Fragment (logic), 010201 computation theory & mathematics, Arbitrary-precision arithmetic, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Automated reasoning, Algorithm, Mathematics, Linear integer arithmetic
Abstract

International audience; In general, first-order predicate logic extended with linear integer arithmetic is undecidable. We show that the Bernays-Schönfinkel-Ramsey fragment (∃ * ∀ *-sentences) extended with a restricted form of linear integer arithmetic is decidable via finite ground instantiation. The identified ground instances can be employed to restrict the search space of existing automated reasoning procedures considerably, e.g., when reasoning about quantified properties of array data structures formalized in Bradley, Manna, and Sipma's array property fragment. Typically, decision procedures for the array property fragment are based on an exhaustive instantiation of universally quantified array indices with all the ground index terms that occur in the formula at hand. Our results reveal that one can get along with significantly fewer instances.

Published
2017
Full Text
View/download PDF

8. Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints

Author

Christoph Weidenbach, Andreas Teucke, Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, de Moura, Leonardo, Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
FOS: Computer and information sciences, Discrete mathematics, Computer Science - Logic in Computer Science, Logic in computer science, Open problem, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Monadic predicate calculus, Logic in Computer Science (cs.LO), Decidability, Automaton, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Fragment (logic), 010201 computation theory & mathematics, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Tree (set theory), Computer Science::Formal Languages and Automata Theory, Mathematics, Resolution (algebra)
Abstract

The monadic shallow linear Horn fragment is well-known to be decidable and has many application, e.g., in security protocol analysis, tree automata, or abstraction refinement. It was a long standing open problem how to extend the fragment to the non-Horn case, preserving decidability, that would, e.g., enable to express non-determinism in protocols. We prove decidability of the non-Horn monadic shallow linear fragment via ordered resolution further extended with dismatching constraints and discuss some applications of the new decidable fragment., Comment: 29 pages, long version of CADE-26 paper

Published
2017
Full Text
View/download PDF

9. On the complexity of the model checking problem

Author

Florent Madelaine, Barnaby Martin, Equipe AMACC - Laboratoire GREYC - UMR6072, Groupe de Recherche en Informatique, Image et Instrumentation de Caen (GREYC), Université de Caen Normandie (UNICAEN), Normandie Université (NU)-Normandie Université (NU)-École Nationale Supérieure d'Ingénieurs de Caen (ENSICAEN), Normandie Université (NU)-Centre National de la Recherche Scientifique (CNRS)-Université de Caen Normandie (UNICAEN), Normandie Université (NU)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes (LIMOS), Université Blaise Pascal - Clermont-Ferrand 2 (UBP)-Université d'Auvergne - Clermont-Ferrand I (UdA)-SIGMA Clermont (SIGMA Clermont)-Ecole Nationale Supérieure des Mines de St Etienne (ENSM ST-ETIENNE)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Ingénieurs de Caen (ENSICAEN), Normandie Université (NU)-Normandie Université (NU)-Université de Caen Normandie (UNICAEN), Normandie Université (NU)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Ingénieurs de Caen (ENSICAEN), Normandie Université (NU), and SIGMA Clermont (SIGMA Clermont)-Université d'Auvergne - Clermont-Ferrand I (UdA)-Ecole Nationale Supérieure des Mines de St Etienne-Centre National de la Recherche Scientifique (CNRS)-Université Blaise Pascal - Clermont-Ferrand 2 (UBP)

Subjects
FOS: Computer and information sciences, Model checking, Computer Science - Logic in Computer Science, General Computer Science, Logic in computer science, Computational complexity theory, General Mathematics, G.2.1, 0102 computer and information sciences, Computational Complexity (cs.CC), 01 natural sciences, Fragment (logic), Constraint satisfaction problem, ComputingMilieux_MISCELLANEOUS, Mathematics, Discrete mathematics, Conjecture, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], F.2.2, F.4.1, Constraint satisfaction, Logic in Computer Science (cs.LO), Computer Science - Computational Complexity, 010201 computation theory & mathematics, Trichotomy (mathematics)
Abstract

The complexity of the model checking problem for various fragments of first-order logic (FO) has attracted much attention over the last two decades, in particular for the fragment induced by ∃ and ∧ and that induced by ∀, ∃, and ∧, which are better known as the constraint satisfaction problem and the quantified constraint satisfaction problem, respectively. The former was conjectured to follow a dichotomy between P and NP-complete by Feder and Vardi [SIAM J. Comput., 28 (1998), pp. 57–104]. For the latter, there are several partial trichotomy results between P, NP-complete, and Pspace-complete, and Chen [Meditations on quantified constraint satisfaction, in Logic and Program Semantics, Springer, Heidelberg, 2012, pp. 35–49] ventured a conjecture regarding Pspace-completeness vs. membership in NP in the presence of constants. We give a comprehensive account of the whole field of the complexity of model checking similar syntactic fragments of FO. The above two fragments are in fact the only ones for which there is currently no known complexity classification. Indeed, we consider all other similar syntactic fragments of FO, induced by the presence or absence of quantifiers and connectives, and fully classify the complexities of the parameterization of the model-checking problem by a finite model D, that is, the expression complexities for certain finite D. Perhaps surprisingly, we show that for most of these fragments, “tractability” is witnessed by a generic solving algorithm which uses quantifier relativization. Our classification methodology relies on tailoring suitably the algebraic approach pioneered by Jeavons, Cohen, and Gyssens [J. ACM, 44 (1997), pp. 527–548] for the constraint satisfaction problem and by B¨orner et al. [Inform. and Comput., 207 (2009), pp. 923–944] for the quantified constraint satisfaction problem. Most fragments under consideration can be relatively easily classified, either directly or using Schaefer’s dichotomy theorems for SAT and QSAT, with the notable exception of the positive equality-free fragment induced by ∃, ∀, ∧, and ∨. This outstanding fragment can also be classified and enjoys a tetrachotomy: according to the model, the corresponding model checking problem is either tractable, NP-complete, co-NP-complete, or Pspace-complete.

Published
2017
Full Text
View/download PDF

10. Locally Finite ω-Languages and Effective Analytic Sets Have the Same Topological Complexity

Author

Finkel, Olivier, Équipe de Logique Mathématique (ELM), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Institut de Mathématiques de Jussieu - Paris Rive Gauche (IMJ-PRG), and Université Pierre et Marie Curie - Paris 6 (UPMC)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)

Subjects
infinite words, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], ω-languages, Wadge hierarchy, Local sentences, formal languages, Borel hierarchy, models of set theory, Mathematics::Logic, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], logic in computer science, [INFO]Computer Science [cs], topological complexity, locally finite languages, decision problems
Abstract

International audience; Local sentences and the formal languages they define were introduced by Ressayre in [Res88]. We prove that locally finite ω-languages and effective analytic sets have the same topological complexity: the Borel and Wadge hierarchies of the class of locally finite ω-languages are equal to the Borel and Wadge hierarchies of the class of effective analytic sets. In particular, for each non-null recursive ordinal α < ω_1^CK there exist some Σ¨0_α-complete and some Π ^0_α-complete locally finite ω-languages, and the supremum of the set of Borel ranks of locally finite ω-languages is the ordinal γ^1_2 , which is strictly greater than the first non-recursive ordinal ω_1^ CK. This gives an answer to the question of the topological complexity of locally finite ω-languages, which was asked by Simonnet [Sim92] and also by Duparc, Finkel, and Ressayre in [DFR01]. Moreover we show that the topological complexity of a locally finite ω-language defined by a local sentence ϕ may depend on the models of the Zermelo-Fraenkel axiomatic system ZFC. Using similar constructions as in the proof of the above results we also show that the equivalence, the inclusion, and the universality problems for locally finite ω-languages are Π^1_2-complete, hence highly undecidable.

Published
2016
Full Text
View/download PDF

11. Extending Nunchaku to Dependent Type Theory

Author

Simon Cruanes, Jasmin Christian Blanchette, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria), Max-Planck-Gesellschaft, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
FOS: Computer and information sciences, Sequence, Computer Science - Logic in Computer Science, Generator (computer programming), Logic in computer science, Programming language, Computer science, lcsh:Mathematics, Short paper, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 02 engineering and technology, Type (model theory), computer.software_genre, lcsh:QA1-939, lcsh:QA75.5-76.95, Logic in Computer Science (cs.LO), Dependent type theory, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, 0202 electrical engineering, electronic engineering, information engineering, lcsh:Electronic computers. Computer science, Partial support, computer, Counterexample
Abstract

Nunchaku is a new higher-order counterexample generator based on a sequence of transformations from polymorphic higher-order logic to first-order logic. Unlike its predecessor Nitpick for Isabelle, it is designed as a stand-alone tool, with frontends for various proof assistants. In this short paper, we present some ideas to extend Nunchaku with partial support for dependent types and type classes, to make frontends for Coq and other systems based on dependent type theory more useful., In Proceedings HaTT 2016, arXiv:1606.05427

Published
2016
Full Text
View/download PDF

12. Incompleteness Theorems, Large Cardinals, and Automata over Infinite Words

Author

Olivier Finkel, Equipe de Logique Mathématique (ELM), Institut de Mathématiques de Jussieu - Paris Rive Gauche (IMJ-PRG (UMR_7586)), Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Institut de Mathématiques de Jussieu - Paris Rive Gauche (IMJ-PRG), Université Pierre et Marie Curie - Paris 6 (UPMC)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Magnus M. Halldorsson and Kazuo Iwama and Naoki Kobayashi and Bettina Speckmann, Equipe de Logique Mathématique, Institut de Mathématiques de Jussieu (IMJ), and Université Pierre et Marie Curie - Paris 6 (UPMC)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Logic in computer science, 2-tape Büchi automaton, Büchi automaton, Mathematics::General Topology, 0102 computer and information sciences, independence from the axiomatic system " ZFC + there exist n inaccessible cardinals ", Gödel's incompleteness theorems, 01 natural sciences, Omega, Combinatorics, models of set theory, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Arithmetic function, inaccessible cardinals, logic in computer science, Automata and formal languages, 0101 mathematics, Mathematics, Discrete mathematics, infinite words, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Context-free grammar, Automaton, 1-counter Büchi automaton, Post correspondence problem, Mathematics::Logic, incompleteness Theorems, large cardinals, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], 010201 computation theory & mathematics, Computer Science::Formal Languages and Automata Theory
Abstract

We prove that there exist some 1-counter Buchi automata $$\mathcal {A}_n$$ for which some elementary properties are independent of theories like $$T_n$$ =: ZFC + "There exist at least n inaccessible cardinals", for integers $$n\ge 1$$ . In particular, if $$T_n$$ is consistent, then " $$L\mathcal {A}_n$$ is Borel", " $$L\mathcal {A}_n$$ is arithmetical", " $$L\mathcal {A}_n$$ is $$\omega $$ -regular", " $$L\mathcal {A}_n$$ is deterministic", and " $$L\mathcal {A}_n$$ is unambiguous" are provable from ZFC + "There exist at least $$n+1$$ inaccessible cardinals" but not from ZFC + "There exist at least n inaccessible cardinals". We prove similar results for infinitary rational relations accepted by 2-tape Buchi automata.

Published
2015
Full Text
View/download PDF

13. {NRCL} - a model building approach to the {Bernays-Schönfinkel} fragment

Author

Gábor Alagi, Christoph Weidenbach, Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Carsten Lutz and Silvio Ranise, Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Discrete mathematics, Monotone polygon, Horn clause, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Logic in computer science, Fragment (logic), Computer science, Backtracking, Modulo, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Tuple, 16. Peace & justice, Resolvent
Abstract

International audience; We combine constrained literals for model representation with key concepts from first-order superposition and propositional conflict-driven clause learning (CDCL) to create the new calculus Non-Redundant Clause Learning (NRCL) deciding the Bernays-Schönfinkel fragment. We use first-order literals constrained by disequalities between tuples of terms for compact model representation. From superposition, NRCL inherits the abstract redundancy criterion and the monotone model operator. CDCL adds the dynamic, conflict-driven search for a model. As a result, NRCL finds a false clause modulo the current model candidate effectively. It guides the derivation of a first-order ordered resolvent that is never redundant. Similar to 1UIP-learning in CDCL, the learned resolvent induces backtracking and, by blocking the previous conflict state via propagation, it enforces progress towards finding a model or a refutation. The non-redundancy result also implies that only finitely many clauses can be generated by NRCL on the Bernays-Schönfinkel fragment, which proves termination.

Published
2015
Full Text
View/download PDF

14. Datalog and Constraint Satisfaction with Infinite Templates

Author

Víctor Dalmau, Manuel Bodirsky, Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Departament de Tecnologies de la Informació i les Comunicacions [Barcelona] (ETIC / UPF), Universitat Pompeu Fabra [Barcelona] (UPF), European Project: 257039,EC:FP7:ERC,ERC-2010-StG_20091028,CSP-COMPLEXITY(2011), Bodirsky, Manuel, Constraint Satisfaction Problems: Algorithms and Complexity - CSP-COMPLEXITY - - EC:FP7:ERC2011-01-01 - 2015-12-31 - 257039 - VALID, and École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Model theory, FOS: Computer and information sciences, [INFO.INFO-AI] Computer Science [cs]/Artificial Intelligence [cs.AI], [INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC], Computer Science - Logic in Computer Science, Datalog, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Logic in computer science, Computational complexity theory, Computer Networks and Communications, 0102 computer and information sciences, 02 engineering and technology, Disjoint sets, Computational Complexity (cs.CC), Constraint satisfaction, Computer Science::Artificial Intelligence, Computer Science::Computational Complexity, 01 natural sciences, Theoretical Computer Science, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, 0101 mathematics, Time complexity, Constraint satisfaction problem, Computer Science::Databases, Mathematics, computer.programming_language, Discrete mathematics, Applied Mathematics, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 16. Peace & justice, Logic in Computer Science (cs.LO), Computational complexity, Computer Science - Computational Complexity, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Countably categorical structures, [MATH.MATH-LO] Mathematics [math]/Logic [math.LO], 020201 artificial intelligence & image processing, [INFO.INFO-CC] Computer Science [cs]/Computational Complexity [cs.CC], computer
Abstract

On finite structures, there is a well-known connection between the expressive power of Datalog, finite variable logics, the existential pebble game, and bounded hypertree duality. We study this connection for infinite structures. This has applications for constraint satisfaction with infinite templates. If the template Gamma is omega-categorical, we present various equivalent characterizations of those Gamma such that the constraint satisfaction problem (CSP) for Gamma can be solved by a Datalog program. We also show that CSP(Gamma) can be solved in polynomial time for arbitrary omega-categorical structures Gamma if the input is restricted to instances of bounded treewidth. Finally, we characterize those omega-categorical templates whose CSP has Datalog width 1, and those whose CSP has strict Datalog width k., Comment: 28 pages. This is an extended long version of a conference paper that appeared at STACS'06. In the third version in the arxiv we have revised the presentation again and added a section that relates our results to formalizations of CSPs using relation algebras

Published
2013

15. On the Expressiveness and Decidability of Higher-Order Process Calculi

Author

Ivan Lanese, Davide Sangiorgi, Alan Schmitt, Jorge Perez Parra, Foundations of Component-based Ubiquitous Systems (FOCUS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)-Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Department of Computer Science and Engineering [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Universidade Nova de Lisboa = NOVA University Lisbon (NOVA), Dipartimento di Scienze dell'Informazione [Bologna] (DISI), Software certification with semantic analysis (CELTIQUE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), ANR-10-BLAN-0305,PiCoq,Vérification Formelle de Composants Distribués(2010), System architecture for reflective distributed computing environments (SARDES), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG), Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), Research partially supported by European Project FET-GC II IST- 2005-16004 SENSORIA, Italian MIUR Project n. 2005015785, 'Logical Foundations of Distributed Systems and Mobile Code', and French ANR project 'CHOCO'., LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria), I. Lanese, J. A. Perez, D. Sangiorgi, A. Schmitt, Fundamental Computing Science, and Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)

Subjects
Logic in computer science, Computer science, Process calculus, Concurrency, 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, 01 natural sciences, Theoretical Computer Science, Process calculi, Turing machine, symbols.namesake, Turing completeness, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Encoding (memory), 0202 electrical engineering, electronic engineering, information engineering, Bisimulation, Equivalence (formal languages), Mathematics, Discrete mathematics, [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Programming language, Expressiveness, 020207 software engineering, Higher-order communication, Computer Science Applications, Decidability, Undecidable problem, Computational Theory and Mathematics, 010201 computation theory & mathematics, Higher order languages, symbols, 020201 artificial intelligence & image processing, computer, Information Systems
Abstract

International audience; In higher-order process calculi the values exchanged in communications may contain processes. A core calculus of higher-order concurrency is studied; it has only the operators necessary to express higher-order communications: input prefix, process output, and parallel composition. By exhibiting a nearly deterministic encoding of Minsky machines, the calculus is shown to be Turing complete and therefore its termination problem is undecidable. Strong bisimilarity, however, is shown to be decidable. Further, the main forms of strong bisimilarity for higher-order processes (higher-order bisimilarity, context bisimilarity, normal bisimilarity, barbed congruence) coincide. They also coincide with their asynchronous versions. A sound and complete axiomatization of bisimilarity is given. Finally, bisimilarity is shown to become undecidable if at least four static (i.e., top-level) restrictions are added to the calculus.

Published
2011
Full Text
View/download PDF

16. Some Problems in Automata Theory Which Depend on the Models of Set Theory

Author

Olivier Finkel, Équipe de Logique Mathématique (ELM), and Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)

Subjects
FOS: Computer and information sciences, [INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC], Computer Science - Logic in Computer Science, Formal Languages and Automata Theory (cs.FL), cardinality problems, General Mathematics, Büchi automaton, Mathematics::General Topology, Computer Science - Formal Languages and Automata Theory, 0102 computer and information sciences, Computational Complexity (cs.CC), 01 natural sciences, Combinatorics, models of set theory, independence from the axiomatic system ZFC, Cardinality, Computer Science::Logic in Computer Science, FOS: Mathematics, Countable set, logic in computer science, Set theory, Automata and formal languages, 0101 mathematics, 2-tape automaton, Continuum hypothesis, Complement (set theory), Mathematics, computational complexity, infinite words, 1-counter automaton, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Mathematics - Logic, Computer Science Applications, Logic in Computer Science (cs.LO), largest thin effective coanalytic set, Computer Science - Computational Complexity, Mathematics::Logic, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], 010201 computation theory & mathematics, Analytical hierarchy, analytical hierarchy, Uncountable set, omega-languages, Logic (math.LO), decision problems, Software, Computer Science::Formal Languages and Automata Theory
Abstract

We prove that some fairly basic questions on automata reading infinite words depend on the models of the axiomatic system ZFC. It is known that there are only three possibilities for the cardinality of the complement of an omega-language $L(A)$ accepted by a B\"uchi 1-counter automaton $A$. We prove the following surprising result: there exists a 1-counter B\"uchi automaton $A$ such that the cardinality of the complement $L(A)^-$ of the omega-language $L(A)$ is not determined by ZFC: (1). There is a model $V_1$ of ZFC in which $L(A)^-$ is countable. (2). There is a model $V_2$ of ZFC in which $L(A)^-$ has cardinal $2^{\aleph_0}$. (3). There is a model $V_3$ of ZFC in which $L(A)^-$ has cardinal $\aleph_1$ with $\aleph_0, Comment: To appear in the journal RAIRO-Theoretical Informatics and Applications

Published
2011
Full Text
View/download PDF

17. Is Ramsey's theorem omega-automatic?

Author

Kuske, Dietrich, Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Inria Nancy Grand Est & Loria, Jean-Yves Marion and Thomas Schwentick, and Loria, Publications

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Logic in computer science, 000 Computer science, knowledge, general works, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Discrete Mathematics (cs.DM), Formal Languages and Automata Theory (cs.FL), 010102 general mathematics, Ramsey theory, Mathematics::General Topology, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Computer Science - Formal Languages and Automata Theory, [INFO.INFO-DM]Computer Science [cs]/Discrete Mathematics [cs.DM], 01 natural sciences, Automata, Logic in Computer Science (cs.LO), 010104 statistics & probability, [INFO.INFO-DM] Computer Science [cs]/Discrete Mathematics [cs.DM], Mathematics::Logic, Computer Science::Discrete Mathematics, Computer Science, F.4.1, 0101 mathematics, Computer Science - Discrete Mathematics
Abstract

International audience; We study the existence of infinite cliques in omega-automatic (hyper-)graphs. It turns out that the situation is much nicer than in general uncountable graphs, but not as nice as for automatic graphs. More specifically, we show that every uncountable omega-automatic graph contains an uncountable co-context-free clique or anticlique, but not necessarily a context-free (let alone regular) clique or anticlique. We also show that uncountable omega-automatic ternary hypergraphs need not have uncountable cliques or anticliques at all.

Published
2010

18. Measurements and confluence in quantum lambda calculi with explicit qubits

Author

Manuel Gadella, Alejandro Díaz-Caro, Jonathan Grattage, Pablo Arrighi, Departamento de Ciencias de la Computación, Departamento de Ciencias de la Computación [Rosario] (DCC), Facultad de Ciencias Exactas, Ingenieria y Agrimensura [Rosario] (FCEIA), Universidad Nacional de Rosario [Santa Fe]-Universidad Nacional de Rosario [Santa Fe]-Facultad de Ciencias Exactas, Ingenieria y Agrimensura [Rosario] (FCEIA), Universidad Nacional de Rosario [Santa Fe]-Universidad Nacional de Rosario [Santa Fe], Calculs algorithmes programmes et preuves (CAPP), Laboratoire d'Informatique de Grenoble (LIG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF), Departamento de Física Teórica, Atómica y Óptica, Universidad de Valladolid [Valladolid] (UVa), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF), and Bob Coecke and Ian Mackie and Prakash Panangaden and Peter Selinger

Subjects
Quantum programming, Pure mathematics, General Computer Science, Logic in computer science, Semantics (computer science), FOS: Physical sciences, 0102 computer and information sciences, 01 natural sciences, Probabilistic rewrite system, Theoretical Computer Science, Operator (computer programming), [PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph], Computer Science::Logic in Computer Science, 0101 mathematics, computer.programming_language, Mathematics, Quantum Physics, Measurement, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Confluence, Term (logic), Confluence, Algebra, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Quantum lambda calculus, 010201 computation theory & mathematics, Qubit, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Programming Languages, Rewriting, Quantum Physics (quant-ph), computer, Computer Science(all)
Abstract

This paper demonstrates how to add a measurement operator to quantum lambda-calculi. A proof of the consistency of the semantics is given through a proof of confluence presented in a sufficiently general way to allow this technique to be used for other languages. The method described here may be applied to probabilistic rewrite systems in general, and to add measurement to more complex languages such as QML or Lineal, which is the subject of further research., Comment: 15 pages. Minor changes: final proceedings version. To appear ENTCS: Proceedings of QPL V - DCV IV, Reykjavik, Iceland, 2008

Published
2008
Full Text
View/download PDF

19. A Graph Abstract Machine Describing Event Structure Composition

Author

Mauro Piccolo, Claudia Faggian, Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Dipartimento di Elettronica e Telecomunicazioni [Torino] (DET), Politecnico di Torino = Polytechnic of Turin (Polito), and Faggian, Claudia

Subjects
Theoretical computer science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], General Computer Science, Logic in computer science, Game semantics, Computer science, Concurrency, 0102 computer and information sciences, 02 engineering and technology, proof nets, computer.software_genre, Semantics, 01 natural sciences, Theoretical Computer Science, Linear Strategies, linear logic, 0202 electrical engineering, electronic engineering, information engineering, ComputingMilieux_MISCELLANEOUS, Geometry of interaction, Programming language, Event Structures, Game Semantics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Directed acyclic graph, Graph, Abstract machine, Linear logic, game semantics, Event structure, 010201 computation theory & mathematics, directed acyclic graph, 020201 artificial intelligence & image processing, Event structures, computer, Ludics, Computer Science(all)
Abstract

Event structures, Game Semantics strategies and Linear Logic proof-nets arise in different domains (concurrency, semantics, proof-theory) but can all be described by means of directed acyclic graphs (dag's). They are all equipped with a specific notion of composition, interaction or normalization.We report on-going work, aiming to investigate the common dynamics which seems to underly these different structures.In this paper we focus on confusion free event structures on one side, and linear strategies [Jean-Yves Girard. Locus solum. Mathematical Structures in Computer Science, 11:301–506, 2001, C. Faggian and F. Maurel. Ludics nets, a game model of concurrent interaction. In Proc. of LICS'05 (Logic in Computer Science). IEEE Computer Society Press, 2005] on the other side. We introduce an abstract machine which is based on (and generalizes) strategies interaction; it processes labelled dag's, and provides a common presentation of the composition at work in these different settings.

Published
2007

20. Completion is an Instance of Abstract Canonical System Inference

Author

Claude Kirchner, Guillaume Burel, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), and Kokichi Futatsugi and Jean-Pierre Jouannaud and José Meseguer

Subjects
equational logic, Theoretical computer science, Logic in computer science, rewriting and deduction, Canonical system, Computer science, Inference, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, proof representation, Computer Science::Logic in Computer Science, Completeness (order theory), ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, 0202 electrical engineering, electronic engineering, information engineering, Equational logic, completion, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Algebraic logic, First-order logic, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, Completeness (statistics), Algorithm, proof ordering
Abstract

http://www.springerlink.com/content/u222753gl333221p/; Abstract canonical systems and inference (ACSI) were introduced to formalize the intuitive notions of good proof and good inference appearing typically in first-order logic or in Knuth-Bendix like completion procedures. Since this abstract framework is intended to be generic, it is of fundamental interest to show its adequacy to represent the main systems of interest. This has been done for ground completion (where all equational axioms are ground) but was still an open question for the general completion process. By showing that the standard completion is an instance of the ACSI framework we close the question. For this purpose, two proof representations, proof terms and proofs by replacement, are compared to built a proof ordering that provides an instantiation adapted to the abstract canonical system framework.

Published
2006
Full Text
View/download PDF

21. Sequent and hypersequent calculi for abelian and Lukasiewicz logics

Author

George Metcalfe, Dov M. Gabbay, Nicola Olivetti, Laboratoire des Sciences de l'Information et des Systèmes (LSIS), Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Arts et Métiers Paristech ENSAM Aix-en-Provence-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS)-Arts et Métiers Paristech ENSAM Aix-en-Provence-Université de Toulon (UTLN)-Aix Marseille Université (AMU), and Domingues Vinhas, William

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, General Computer Science, Logic in computer science, Logic, 0102 computer and information sciences, MV-algebra, [INFO] Computer Science [cs], 01 natural sciences, Theoretical Computer Science, Mathematics::Quantum Algebra, Computer Science::Logic in Computer Science, [INFO]Computer Science [cs], Sequent, 0101 mathematics, Abelian group, Łukasiewicz logic, ComputingMilieux_MISCELLANEOUS, Mathematics, Discrete mathematics, I.2.3, 010102 general mathematics, Logic in Computer Science (cs.LO), Algebra, Mathematics::Logic, Computational Mathematics, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, F.4.1, Computer Science::Programming Languages, Analytic proof
Abstract

We present two embeddings of infinite-valued Lukasiewicz logic L into Meyer and Slaney's abelian logic A, the logic of lattice-ordered abelian groups. We give new analytic proof systems for A and use the embeddings to derive corresponding systems for L. These include: hypersequent calculi for A and L and terminating versions of these calculi; labelled single sequent calculi for A and L of complexity co-NP; unlabelled single sequent calculi for A and L., Comment: 35 pages, 1 figure

Published
2005

22. Soft lambda-calculus: a language for polynomial time computation

Author

Virgile Mogbil, Patrick Baillot, arXiv, Import, Laboratoire d'Informatique de Paris-Nord (LIPN), Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS), AS CNRS 'Méthodes formelles pour la mobilité' et ACI CRISS, and Baillot, Patrick

Subjects
FOS: Computer and information sciences, [INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC], Computer Science - Logic in Computer Science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Logic in computer science, Computer science, F.4, Linear logic, implicit computational complexity, 0102 computer and information sciences, Computational Complexity (cs.CC), 01 natural sciences, polynomial time complexity, Computer Science::Logic in Computer Science, Implicit computational complexity, F.4.1, F.4.2, 0101 mathematics, recursive types, computer.programming_language, Discrete mathematics, Soft computing, Soft linear logic, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], lambda-calculus, Logic in Computer Science (cs.LO), Computer Science - Computational Complexity, Type theory, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, Minimal logic, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Programming Languages, [INFO.INFO-CC] Computer Science [cs]/Computational Complexity [cs.CC], Affine logic, Lambda calculus, computer
Abstract

Soft linear logic ([Lafont02]) is a subsystem of linear logic characterizing the class PTIME. We introduce Soft lambda-calculus as a calculus typable in the intuitionistic and affine variant of this logic. We prove that the (untyped) terms of this calculus are reducible in polynomial time. We then extend the type system of Soft logic with recursive types. This allows us to consider non-standard types for representing lists. Using these datatypes we examine the concrete expressivity of Soft lambda-calculus with the example of the insertion sort algorithm., 20 pages

Published
2003

23. One Binary Horn Clause is Enough

Author

Jörg Würtz, Jean-Christophe Routier, Philippe Devienne, Patrick Lebègue, Laboratoire d'Informatique Fondamentale de Lille (LIFL), Université de Lille, Sciences et Technologies-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lille, Sciences Humaines et Sociales-Centre National de la Recherche Scientifique (CNRS), Systèmes Multi-Agents et Comportements (SMAC), Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Deutsches Forschungszentrum für Künstliche Intelligenz GmbH = German Research Center for Artificial Intelligence (DFKI), Enjalbert, Patrice and Mayr, E.W. and Wagner, and K.W.

Subjects
Scheme (programming language), Horn clause, Logic in computer science, Computer science, Binary number, 0102 computer and information sciences, computer.software_genre, 01 natural sciences, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], 0101 mathematics, Fifth-generation programming language, Computer Science::Databases, computer.programming_language, Declarative programming, [QFIN.GN]Quantitative Finance [q-fin]/General Finance [q-fin.GN], Class (computer programming), [INFO.INFO-GT]Computer Science [cs]/Computer Science and Game Theory [cs.GT], Programming language, 010102 general mathematics, [INFO.INFO-CE]Computer Science [cs]/Computational Engineering, Finance, and Science [cs.CE], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Structured programming, 010201 computation theory & mathematics, [INFO.INFO-MA]Computer Science [cs]/Multiagent Systems [cs.MA], Computer Science::Programming Languages, computer
Abstract

This paper proposes an equivalent form of the famous Bohm-Jacopini theorem for declarative languages. C. Bohm and G. Jacopini [1] proved that all programming can be done with at most one single whiledo. That result is cited as a mathematical justification for structured programming. A similar result can be shown for declarative programming. Indeed the simplest class of recursive programs in Horn clause languages can be defined by the following scheme

Published
1994

Catalog

Books, media, physical & digital resources
See catalog results