13 Search Results for "Escobar, Santiago"

Volume

OASIcs, Volume 46

2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

WPTE 2015, July 2, 2015, Warsaw, Poland

Editors: Yuki Chiba, Santiago Escobar, Naoki Nishida, David Sabel, and Manfred Schmidt-Schauß

Document
DOI: 10.4230/LIPIcs.ITP.2025.12
Automatically Generalizing Proofs and Statements

Authors: Anshula Gandhi, Anand Rao Tadipatri, and Timothy Gowers

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
We present an algorithm, developed in the Lean programming language, to automatically generalize mathematical proofs. The algorithm, which builds on work by Olivier Pons, advances state-of-the-art proof generalization by robustly generalizing repeated and related constants, as well as abstracting out hypotheses implicitly concerning them. We also discuss the role of proof generalization in conjecturing, learning from failure, and other aspects of mathematical proof discovery.
Cite as

Anshula Gandhi, Anand Rao Tadipatri, and Timothy Gowers. Automatically Generalizing Proofs and Statements. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{gandhi_et_al:LIPIcs.ITP.2025.12,
  author =	{Gandhi, Anshula and Tadipatri, Anand Rao and Gowers, Timothy},
  title =	{{Automatically Generalizing Proofs and Statements}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{12:1--12:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.12},
  URN =		{urn:nbn:de:0030-drops-246104},
  doi =		{10.4230/LIPIcs.ITP.2025.12},
  annote =	{Keywords: automated reasoning, automated theorem proving, interactive theorem proving, formalization of mathematics, generalization, Lean theorem prover, Lean tactic}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.7
Combining Generalization Algorithms in Regular Collapse-Free Theories

Authors: Mauricio Ayala-Rincón, David M. Cerna, Temur Kutsia, and Christophe Ringeissen

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
We look at the generalization problem modulo some equational theories. This problem is dual to the unification problem: given two input terms, we want to find a common term whose respective two instances are equivalent to the original terms modulo the theory. There exist algorithms for finding generalizations over various equational theories. We focus on modular construction of equational generalization algorithms for the union of signature-disjoint theories. Specifically, we consider the class of regular and collapse-free theories, showing how to combine existing generalization algorithms to produce specific solutions in these cases. Additionally, we identify a class of theories that admit a generalization algorithm based on the application of axioms to resolve the problem. To define this class, we rely on the notion of syntactic theories, a concept originally introduced to develop unification procedures similar to the one known for syntactic unification. We demonstrate that syntactic theories are also helpful in developing generalization procedures similar to those used for syntactic generalization.
Cite as

Mauricio Ayala-Rincón, David M. Cerna, Temur Kutsia, and Christophe Ringeissen. Combining Generalization Algorithms in Regular Collapse-Free Theories. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2025.7,
  author =	{Ayala-Rinc\'{o}n, Mauricio and Cerna, David M. and Kutsia, Temur and Ringeissen, Christophe},
  title =	{{Combining Generalization Algorithms in Regular Collapse-Free Theories}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.7},
  URN =		{urn:nbn:de:0030-drops-236228},
  doi =		{10.4230/LIPIcs.FSCD.2025.7},
  annote =	{Keywords: Generalization, Anti-unification, Equational theories, Combination}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.8
The Unification Type of an Equational Theory May Depend on the Instantiation Preorder

Authors: Franz Baader and Oliver Fernández Gil

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
The unification type of an equational theory is defined using a preorder on substitutions, called the instantiation preorder, whose scope is either restricted to the variables occurring in the unification problem, or unrestricted such that all variables are considered. It has been known for more than three decades that the unification type of an equational theory may vary, depending on which instantiation preorder is used. More precisely, it was shown in 1991 that the theory ACUI of an associative, commutative, and idempotent binary function symbol with a unit is unitary w.r.t. the restricted instantiation preorder, but not unitary w.r.t. the unrestricted one. In 2016 this result was strengthened by showing that the unrestricted type of this theory also cannot be finitary. Here, we considerably improve on this result by proving that ACUI is infinitary w.r.t. the unrestricted instantiation preorder, thus precluding type zero. We also show that, w.r.t. this preorder, the unification type of ACU (where idempotency is removed from the axioms) and of AC (where additionally the unit is removed) is infinitary, though it is respectively unitary and finitary in the restricted case. In the other direction, we prove (using the example of unification in the description logic EL) that the unification type may actually improve from type zero to infinitary when switching from the restricted instantiation preorder to the unrestricted one. In addition, we establish some general results on the relationship between the two instantiation preorders.
Cite as

Franz Baader and Oliver Fernández Gil. The Unification Type of an Equational Theory May Depend on the Instantiation Preorder. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 8:1-8:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{baader_et_al:LIPIcs.FSCD.2025.8,
  author =	{Baader, Franz and Fern\'{a}ndez Gil, Oliver},
  title =	{{The Unification Type of an Equational Theory May Depend on the Instantiation Preorder}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{8:1--8:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.8},
  URN =		{urn:nbn:de:0030-drops-236230},
  doi =		{10.4230/LIPIcs.FSCD.2025.8},
  annote =	{Keywords: Unification type, Instantiation preorder, Equational theories, Modal and Description Logics}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.WPTE.2015
OASIcs, Volume 46, WPTE'15, Complete Volume

Authors: Yuki Chiba, Santiago Escobar, Naoki Nishida, David Sabel, and Manfred Schmidt-Schauß

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
OASIcs, Volume 46, WPTE'15, Complete Volume
Cite as

2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Proceedings{chiba_et_al:OASIcs.WPTE.2015,
  title =	{{OASIcs, Volume 46, WPTE'15, Complete Volume}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015},
  URN =		{urn:nbn:de:0030-drops-52644},
  doi =		{10.4230/OASIcs.WPTE.2015},
  annote =	{Keywords: Conference proceedings, Concurrent Programming, Formal Definitions and Theory, Specifying and Verifying and Reasoning about Programs, Semantics of Programming Languages, Mathematical Logic, Grammars and Other Rewriting Systems, Deduction and Theorem Proving}
}
Document
Front Matter
DOI: 10.4230/OASIcs.WPTE.2015.i
Frontmatter, Table of Contents, Preface, Workshop Organization

Authors: Yuki Chiba, Santiago Escobar, Naoki Nishida, David Sabel, and Manfred Schmidt-Schauß

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
Frontmatter, Table of Contents, Preface, Workshop Organization
Cite as

2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. i-xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{chiba_et_al:OASIcs.WPTE.2015.i,
  author =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  title =	{{Frontmatter, Table of Contents, Preface, Workshop Organization}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{i--xvi},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.i},
  URN =		{urn:nbn:de:0030-drops-51765},
  doi =		{10.4230/OASIcs.WPTE.2015.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization}
}
Document
Invited Talk
DOI: 10.4230/OASIcs.WPTE.2015.1
Mechanizing Meta-Theory in Beluga (Invited Talk)

Authors: Brigitte Pientka

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. In this talk, I will survey the proof environment Beluga. To specify formal systems and represent derivations within them, Beluga provides a sophisticated infrastructure based on the logical framework LF; in particular, its infrastructure not only supports modelling binders via binders in LF, but extends and generalizes LF with first-class contexts to abstract over a set of assumptions, contextual objects to model derivations that depend on assumptions, and first-class simultaneous substitutions to relate contexts. These extensions allow us to directly support key and common concepts that frequently arise when describing formal systems and derivations within them. To reason about formal systems, Beluga provides a dependently typed functional language for implementing inductive proofs about derivations as recursive functions on contextual objects following the Curry-Howard isomorphism. Recently, the Beluga system has also been extended with a totality checker which guarantees that recursive programs are well-founded and correspond to inductive proofs and an interactive program development environment to support incremental proof / program construction. Taken together these extensions enable direct and compact mechanizations. To demonstrate Beluga's strength, we develop a weak normalization proof using logical relations. The Beluga system together with examples is available from http://complogic.cs.mcgill.ca/beluga.
Cite as

Brigitte Pientka. Mechanizing Meta-Theory in Beluga (Invited Talk). In 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, p. 1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{pientka:OASIcs.WPTE.2015.1,
  author =	{Pientka, Brigitte},
  title =	{{Mechanizing Meta-Theory in Beluga}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{1--1},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.1},
  URN =		{urn:nbn:de:0030-drops-51770},
  doi =		{10.4230/OASIcs.WPTE.2015.1},
  annote =	{Keywords: Type systems, Dependent Types, Logical Frameworks}
}
Document
DOI: 10.4230/OASIcs.WPTE.2015.3
Head reduction and normalization in a call-by-value lambda-calculus

Authors: Giulio Guerrieri

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
Recently, a standardization theorem has been proven for a variant of Plotkin's call-by-value lambda-calculus extended by means of two commutation rules (sigma-reductions): this result was based on a partitioning between head and internal reductions. We study the head normalization for this call-by-value calculus with sigma-reductions and we relate it to the weak evaluation of original Plotkin's call-by-value lambda-calculus. We give also a (non-deterministic) normalization strategy for the call-by-value lambda-calculus with sigma-reductions.
Cite as

Giulio Guerrieri. Head reduction and normalization in a call-by-value lambda-calculus. In 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. 3-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{guerrieri:OASIcs.WPTE.2015.3,
  author =	{Guerrieri, Giulio},
  title =	{{Head reduction and normalization in a call-by-value lambda-calculus}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{3--17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.3},
  URN =		{urn:nbn:de:0030-drops-51789},
  doi =		{10.4230/OASIcs.WPTE.2015.3},
  annote =	{Keywords: sequentialization, lambda-calculus, sigma-reduction, call-by-value, head reduction, internal reduction, (strong) normalization, evaluation, confluence}
}
Document
DOI: 10.4230/OASIcs.WPTE.2015.19
Towards Modelling Actor-Based Concurrency in Term Rewriting

Authors: Adrián Palacios and Germán Vidal

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
In this work, we introduce a scheme for modelling actor systems within sequential term rewriting. In our proposal, a TRS consists of the union of three components: the functional part (which is specific of a system), a set of rules for reducing concurrent actions, and a set of rules for defining a particular scheduling policy. A key ingredient of our approach is that concurrent systems are modelled by terms in which concurrent actions can never occur inside user-defined function calls. This assumption greatly simplifies the definition of the semantics for concurrent actions, since no term traversal will be needed. We prove that these systems are well defined in the sense that concurrent actions can always be reduced. Our approach can be used as a basis for modelling actor-based concurrent programs, which can then be analyzed using existing techniques for term rewrite systems.
Cite as

Adrián Palacios and Germán Vidal. Towards Modelling Actor-Based Concurrency in Term Rewriting. In 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. 19-29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{palacios_et_al:OASIcs.WPTE.2015.19,
  author =	{Palacios, Adri\'{a}n and Vidal, Germ\'{a}n},
  title =	{{Towards Modelling Actor-Based Concurrency in Term Rewriting}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{19--29},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.19},
  URN =		{urn:nbn:de:0030-drops-51792},
  doi =		{10.4230/OASIcs.WPTE.2015.19},
  annote =	{Keywords: concurrency, actor model, rewriting}
}
Document
DOI: 10.4230/OASIcs.WPTE.2015.31
Observing Success in the Pi-Calculus

Authors: David Sabel and Manfred Schmidt-Schauß

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
A contextual semantics - defined in terms of successful termination and may- and should-convergence - is analyzed in the synchronous pi-calculus with replication and a constant Stop to denote success. The contextual ordering is analyzed, some nontrivial process equivalences are proved, and proof tools for showing contextual equivalences are provided. Among them are a context lemma and new notions of sound applicative similarities for may- and should-convergence. A further result is that contextual equivalence in the pi-calculus with Stop conservatively extends barbed testing equivalence in the (Stop-free) pi-calculus and thus results on contextual equivalence can be transferred to the (Stop-free) pi-calculus with barbed testing equivalence.
Cite as

David Sabel and Manfred Schmidt-Schauß. Observing Success in the Pi-Calculus. In 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. 31-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{sabel_et_al:OASIcs.WPTE.2015.31,
  author =	{Sabel, David and Schmidt-Schau{\ss}, Manfred},
  title =	{{Observing Success in the Pi-Calculus}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{31--46},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.31},
  URN =		{urn:nbn:de:0030-drops-51808},
  doi =		{10.4230/OASIcs.WPTE.2015.31},
  annote =	{Keywords: Concurrency, Process calculi, Pi-calculus, Rewriting, Semantics}
}
Document
DOI: 10.4230/OASIcs.WPTE.2015.47
Formalizing Bialgebraic Semantics in PVS 6.0

Authors: Sjaak Smetsers, Ken Madlener, and Marko van Eekelen

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

Abstract
Both operational and denotational semantics are prominent approaches for reasoning about properties of programs and programming languages. In the categorical framework developed by Turi and Plotkin both styles of semantics are unified using a single, syntax independent format, known as GSOS, in which the operational rules of a language are specified. From this format, the operational and denotational semantics are derived. The approach of Turi and Plotkin is based on the categorical notion of bialgebras. In this paper we specify this work in the theorem prover PVS, and prove the adequacy theorem of this formalization. One of our goals is to investigate whether PVS is adequately suited for formalizing metatheory. Indeed, our experiments show that the original categorical framework can be formalized conveniently. Additionally, we present a GSOS specification for the simple imperative programming language While, and execute the derived semantics for a small example program.
Cite as

Sjaak Smetsers, Ken Madlener, and Marko van Eekelen. Formalizing Bialgebraic Semantics in PVS 6.0. In 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. 47-61, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{smetsers_et_al:OASIcs.WPTE.2015.47,
  author =	{Smetsers, Sjaak and Madlener, Ken and van Eekelen, Marko},
  title =	{{Formalizing Bialgebraic Semantics in PVS 6.0}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{47--61},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.47},
  URN =		{urn:nbn:de:0030-drops-51811},
  doi =		{10.4230/OASIcs.WPTE.2015.47},
  annote =	{Keywords: operational semantics, denotational semantics, bialgebras, distributive laws, adequacy, theorem proving, PVS, WHILE}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.81
Abstract Logical Model Checking of Infinite-State Systems Using Narrowing

Authors: Kyungmin Bae, Santiago Escobar, and José Meseguer

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
A concurrent system can be naturally specified as a rewrite theory R = (Sigma, E, R) where states are elements of the initial algebra of terms modulo E and concurrent transitions are axiomatized by the rewrite rules R. Under simple conditions, narrowing with rules R modulo equations E can be used to symbolically represent the system's state space by means of terms with logical variables. We call this symbolic representation a "logical state space" and it can also be used for model checking verification of LTL properties. Since in general such a logical state space can be infinite, we propose several abstraction techniques for obtaining either an over-approximation or an under-approximation of the logical state space: (i) a folding abstraction that collapses patterns into more general ones, (ii) an easy-to-check method to define (bisimilar) equational abstractions, and (iii) an iterated bounded model checking method that can detect if a logical state space within a given bound is complete. We also show that folding abstractions can be faithful for safety LTL properties, so that they do not generate any spurious counterexamples. These abstraction methods can be used in combination and, as we illustrate with examples, can be effective in making the logical state space finite. We have implemented these techniques in the Maude system, providing the first narrowing-based LTL model checker we are aware of.
Cite as

Kyungmin Bae, Santiago Escobar, and José Meseguer. Abstract Logical Model Checking of Infinite-State Systems Using Narrowing. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 81-96, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{bae_et_al:LIPIcs.RTA.2013.81,
  author =	{Bae, Kyungmin and Escobar, Santiago and Meseguer, Jos\'{e}},
  title =	{{Abstract Logical Model Checking of Infinite-State Systems Using Narrowing}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{81--96},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.81},
  URN =		{urn:nbn:de:0030-drops-40554},
  doi =		{10.4230/LIPIcs.RTA.2013.81},
  annote =	{Keywords: model checking, infinite states, rewrite theories, narrowing}
}
Document
DOI: 10.4230/LIPIcs.RTA.2011.31
Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6

Authors: Francisco Duran, Steven Eker, Santiago Escobar, Jose Meseguer, and Carolyn Talcott

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
This paper introduces some novel features of Maude 2.6 focusing on the variants of a term. Given an equational theory (Sigma,Ax cup E), the E,Ax-variants of a term t are understood as the set of all pairs consisting of a substitution sigma and the E,Ax-canonical form of t sigma. The equational theory (Ax cup E ) has the finite variant property if there is a finite set of most general variants. We have added support in Maude 2.6 for: (i) order-sorted unification modulo associativity, commutativity and identity, (ii) variant generation, (iii) order-sorted unification modulo finite variant theories, and (iv) narrowing-based symbolic reachability modulo finite variant theories. We also explain how these features have a number of interesting applications in areas such as unification theory, cryptographic protocol verification, business processes, and proofs of termination, confluence and coherence.
Cite as

Francisco Duran, Steven Eker, Santiago Escobar, Jose Meseguer, and Carolyn Talcott. Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 31-40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{duran_et_al:LIPIcs.RTA.2011.31,
  author =	{Duran, Francisco and Eker, Steven and Escobar, Santiago and Meseguer, Jose and Talcott, Carolyn},
  title =	{{Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{31--40},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.31},
  URN =		{urn:nbn:de:0030-drops-31211},
  doi =		{10.4230/LIPIcs.RTA.2011.31},
  annote =	{Keywords: Rewriting logic, narrowing, unification, variants}
}
  • Refine by Type
  • 12 Document/PDF
  • 3 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 3 2025
  • 8 2015
  • 1 2013
  • 1 2011

  • Refine by Author
  • 4 Escobar, Santiago
  • 3 Sabel, David
  • 3 Schmidt-Schauß, Manfred
  • 2 Chiba, Yuki
  • 2 Nishida, Naoki
  • Show More...

  • Refine by Series/Journal
  • 5 LIPIcs
  • 7 OASIcs

  • Refine by Classification
  • 2 Theory of computation → Automated reasoning
  • 2 Theory of computation → Equational logic and rewriting
  • 1 Computing methodologies → Symbolic and algebraic manipulation
  • 1 Theory of computation → Description logics
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 2 Equational theories
  • 2 narrowing
  • 1 (strong) normalization
  • 1 Anti-unification
  • 1 Combination
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact