Superposition-based Decision Procedures for Minimal Models

First-order Theorem Proving for Fixed Domain and Minimal Model Validity

Autori

• Matthias Horbach

Parametri

• 216 pagine
• 8 ore di lettura

• Computer, IT, programmazione

Maggiori informazioni sul libro

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.

Lingua: Inglese

Pubblicato: 2011

(In brossura)