Uniform Derivation of Decision Procedures by Superposition

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.

• Type: Conference
• Year: 2001
• Where: CSL
• Authors: Alessandro Armando, Silvio Ranise, Michaël Rusinowitch
• Keywords: Automated Reasoning, CSL 2001, Decision Procedure, Well-known Superposition-based Inference, first-order Equational Logic