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