Modular proof systems for partial functions with Evans equality

The paper presents a modular superposition calculus for the combination of firstorder theories involving both total and partial functions. The modularity of the calculus is a consequence of the fact that all the inferences are pure

• Type: Journal
• Year: 2006
• Where: IANDC
• Authors: Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann
• Keywords: Calculus, Firstorder Theories, IANDC 2006, Modular Superposition Calculus