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 ...