Superposition-based Decision Procedures for Minimal Models

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

Autor*innen

• Matthias Horbach

Parameter

• 216 Seiten
• 8 Lesestunden

• Informatik & Programmierung

Mehr zum Buch

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.

• Sprache: Englisch
• Erscheinungsdatum: 2011
• Einband: Paperback