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.
Uniform derivation of decision procedures by superposition / Armando, A.; Ranise, S.; Rusinowitch, M.. - 2142:(2001), pp. 513-527. (Intervento presentato al convegno 15th International Workshop on Computer Science Logic, CSL 2001 and 10th Annual Conference of the European Association for Computer Science Logic, EACSL 2001 tenutosi a fra nel 2001) [10.1007/3-540-44802-0_36].
Uniform derivation of decision procedures by superposition
Ranise S.;
2001-01-01
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
