Superposition-based Decision Procedures for Minimal Models
First-order Theorem Proving for Fixed Domain and Minimal Model Validity
- 216pages
- 8 heures de lecture
Focusing on a novel approach to reasoning within first-order logic, the book introduces a superposition calculus that explicitly represents existentially quantified variables without resorting to Skolemization. By utilizing additional constraints for clause annotation, it maintains soundness and refutational completeness for fixed domain semantics. The author, Matthias Horbach, explores the implications of this calculus for proving universal properties and minimal model validity, offering new decision procedures for specific classes of theories, enhancing the understanding of Herbrand models.
