Superposition-based Decision Procedures for Minimal Models

More about the book

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.