Search

Your search keyword '"Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM)"' showing total 3 results
Start Over Author "Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM)" Publisher elsevier bv
3 results on '"Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM)"'

1. Unification of drags and confluence of drag rewriting

Author

Jouannaud, Jean-Pierre, Orejas, Fernando, Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Universitat Politècnica de Catalunya [Barcelona] (UPC), Jouannaud, Jean-Pierre, Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire de Méthodes Formelles, Université de Paris-Saclay, Université de Paris Saclay, Universitat Politècnica de Catalunya. Departament de Ciències de la Computació, and Universitat Politècnica de Catalunya. ALBCOM - Algorísmia, Bioinformàtica, Complexitat i Mètodes Formals

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], unification, InformationSystems_INFORMATIONINTERFACESANDPRESENTATION(e.g.,HCI), Logic, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], GeneralLiterature_MISCELLANEOUS, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Theoretical Computer Science, Physics::Fluid Dynamics, Computer Science::Logic in Computer Science, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Drags, Algorismes computacionals, ComputingMethodologies_COMPUTERGRAPHICS, graphs, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Confluence, ACM: D.: Software, Computer algorithms, ACM: F.: Theory of Computation, Informàtica::Informàtica teòrica::Algorísmica i teoria de la complexitat [Àrees temàtiques de la UPC], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, Unification, [INFO.INFO-CL] Computer Science [cs]/Computation and Language [cs.CL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, confluence, Computer Science::Programming Languages, Astrophysics::Earth and Planetary Astrophysics, Graphs, Software
Abstract

Drags are a recent, natural generalization of terms which admit arbitrary cycles. A key aspect of drags is that they can be equipped with a composition operator so that rewriting amounts to replace a drag by another in a composition. In this paper, we develop a unification algorithm for drags that allows to check the local confluence property of a set of drag rewrite rules. This work is partially supported by MCIN/AEI /10.13039/501100011033 under grant PID2020-112581GB-C21.

Published
2023
Full Text
View/download PDF

2. Drags: A compositional algebraic framework for graph rewriting

Author

Jean-Pierre Jouannaud, Nachum Dershowitz, Tel Aviv University (TAU), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Spécification et Vérification (LSV), Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Université Paris-Saclay, Deducteam, and Tel Aviv University [Tel Aviv]

Subjects
Vertex (graph theory), General Computer Science, Computer science, Generalization, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Term algebra, ACM: G.: Mathematics of Computing, Theoretical Computer Science, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, Drags, 0202 electrical engineering, electronic engineering, information engineering, [INFO]Computer Science [cs], Algebraic number, Graph rewriting, symmetric monoidal category, Symmetric monoidal category, Function (mathematics), Graph, rewriting, Vertex (geometry), Algebra, 010201 computation theory & mathematics, Computer Science::Programming Languages, 020201 artificial intelligence & image processing, Rewriting, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], Graphs, MathematicsofComputing_DISCRETEMATHEMATICS
Abstract

International audience; We are interested in a natural generalization of term-rewriting techniques to what we call drags, viz. finite, directed, ordered, rooted multigraphs, each vertex of which is labeled by a function symbol. To this end, we develop a rich algebra of drags that generalizes the familiar term algebra and its associated rewriting capabilities. Viewing graphs as terms provides an initial building block for rewriting with such graphs, one that should impact the many areas where computations take place on graphs.

Published
2019
Full Text
View/download PDF

3. On the Convergence of Reduction-based and Model-based Methods in Proof Theory

Author

Gilles Dowek, Types, Logic and computing (TYPICAL), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), and Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Constructive proof, General Computer Science, Logic, Computer science, Theoretical Computer Science, Reduction (complexity), models, Computer-assisted proof, Convergence (routing), Calculus, Applied mathematics, Structural proof theory, Mathematics, Discrete mathematics, Proof complexity, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], reducibility candidates, Logic in Computer Science (cs.LO), truth values algebras, Transformation (function), Proof theory, Cut elimination, Computer Science(all), Analytic proof
Abstract

In the recent past, the reduction-based and the model-based methods to prove cut elimination have converged, so that they now appear just as two sides of the same coin. This paper details some of the steps of this transformation.

Published
2008
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results