Now showing items 1-3 of 3

Order-Sorted Equality Enrichments Modulo Axioms

Gutiérrez, Raúl; Meseguer, José; Rocha, Camilo (SpringerBerlin., 2012)

Built-in equality and inequality predicates based on comparison of canonical forms in algebraic specifications are frequently used because they are handy and efficient. However, their use places algebraic specifications ...
Proving Safety Properties of Rewrite Theories

Rocha, Camilo; Meseguer, José (SpringerBerlín, 2011)

Rewrite theories are a general and expressive formalism for specifying concurrent systems in which states are axiomatized by equations and transitions among states are axiomatized by rewrite rules. We present a deductive ...
Theorem Proving Modulo Based on Boolean Equational Procedures

Rocha, Camilo; Meseguer, José (Springer, 2008)

Deduction with inference rules modulo computation rules plays an important role in automated deduction as an effective method for scaling up. We present four equational theories that are isomorphic to the traditional Boolean ...

Envíos recientes

Order-Sorted Equality Enrichments Modulo Axioms
...
Gutiérrez, Raúl | 2012

Built-in equality and inequality predicates based on comparison of canonical forms in algebraic specifications are frequently used because they are handy and efficient. However, their use places algebraic specifications with initial algebra semantics beyond the pale of theorem proving tools based, for example, on explicit or inductionless induction techniques, and of other formal tools for checking key properties such as confluence, termination, and sufficient completeness. Such specifications would instead be amenable to formal analysis if an equationally-defined equality predicate enriching the algebraic data types were to be added to them. Furthermore, having an equationally-defined equality predicate is very useful in its own right, particularly in inductive theorem proving. Is it possible to effectively define a theory transformation E↦E≃ that extends an algebraic specification E to a specification E≃ having an equationally-defined equality predicate? This paper answers this question in the affirmative for a broad class of order-sorted conditional specifications E that are sort-decreasing, ground confluent, and operationally terminating modulo axioms B and have a subsignature of constructors. The axioms B can consist of associativity, or commutativity, or associativity-commutativity axioms, so that the constructors are free modulo B. We prove that the transformation E↦E≃ preserves all the just-mentioned properties of E . The transformation has been automated in Maude using reflection and is used in several Maude formal tools.

LEER
Proving Safety Properties of Rewrite Theories
...
Rocha, Camilo | 2011

Rewrite theories are a general and expressive formalism for specifying concurrent systems in which states are axiomatized by equations and transitions among states are axiomatized by rewrite rules. We present a deductive approach for verifying safety properties of rewrite theories in which all formal temporal reasoning about concurrent transitions is ultimately reduced to purely equational inductive reasoning. Narrowing modulo axioms is extensively used in our inference system to further simplify the equational proof obligations to which all proofs of safety formulas are ultimately reduced. In this way, existing equational reasoning techniques and tools can be directly applied to verify safety properties of concurrent systems. We report on the implementation of this deductive system in the Maude Invariant Analyzer tool, which provides a substantial degree of automation and can automatically discharge many proof obligations without user intervention.

LEER
Theorem Proving Modulo Based on Boolean Equational Procedures
...
Rocha, Camilo | 2008

Deduction with inference rules modulo computation rules plays an important role in automated deduction as an effective method for scaling up. We present four equational theories that are isomorphic to the traditional Boolean theory and show that each of them gives rise to a Boolean decision procedure based on a canonical rewrite system modulo associativity and commutativity. Then, we present two modular extensions of our decision procedure for Dijkstra-Scholten propositional logic to the Sequent Calculus for First Order Logic and to the Syllogistic Logic with Complements of L. Moss. These extensions take the form of rewrite theories that are sound and complete for performing deduction modulo their equational parts and exhibit good mechanization properties. We illustrate the practical usefulness of this approach by a direct implementation of one of these theories in Maude rewriting logic language, and automatically proving a challenge benchmark in theorem proving.

LEER