We show how a well-known superposition-based inference system for first-order equational logic can be used almost directly for deciding satisfiability in various theories including lists, encryption, extensional arrays, extensional finite sets, and combinations of them. We also give a superposition-based decision procedure for homomorphism.

A rewriting approach to satisfiability procedures / Armando, A.; Ranise, S.; Rusinowitch, M.. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 183:2(2003), pp. 140-164. [10.1016/S0890-5401(03)00020-8]

A rewriting approach to satisfiability procedures

Ranise S.;
2003-01-01

Abstract

We show how a well-known superposition-based inference system for first-order equational logic can be used almost directly for deciding satisfiability in various theories including lists, encryption, extensional arrays, extensional finite sets, and combinations of them. We also give a superposition-based decision procedure for homomorphism.
2003
2
Armando, A.; Ranise, S.; Rusinowitch, M.
A rewriting approach to satisfiability procedures / Armando, A.; Ranise, S.; Rusinowitch, M.. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 183:2(2003), pp. 140-164. [10.1016/S0890-5401(03)00020-8]
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333270
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 98
  • ???jsp.display-item.citation.isi??? 72
social impact