Skip to Main content Skip to Navigation
Reports

Uniform Derivation of Decision Procedures by Superposition

Alessandro Armando Silvio Ranise 1 Michaël Rusinowitch 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We show how a well-known superposition-based inference system for first-order equational logic can be used almost directly as a decision procedure for various theories including lists, arrays, extensional arrays and combinations of them. We also give a superposition-based decision procedure for homomorphism.
Complete list of metadatas

https://hal.inria.fr/inria-00072474
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:03:34 AM
Last modification on : Wednesday, January 8, 2020 - 2:16:59 PM
Document(s) archivé(s) le : Sunday, April 4, 2010 - 11:09:27 PM

Identifiers

  • HAL Id : inria-00072474, version 1

Collections

Citation

Alessandro Armando, Silvio Ranise, Michaël Rusinowitch. Uniform Derivation of Decision Procedures by Superposition. [Research Report] RR-4151, INRIA. 2001, pp.13. ⟨inria-00072474⟩

Share

Metrics

Record views

197

Files downloads

243