An Abstract Machine for Model Generation with PHUR Tableaux (Extended Abstract)

Machine for Model Generation with PUHR Tableaux (Extended Abstract) Alexander von Drach, Tim Geisler, Sven Panne, David Sacher In: Proc 13th Workshop Logische Programmierung (WLP '98), TU Wien, Oct. 1998 http://www.pms.informatik.uni-muenchen.de/publikationen Forschungsbericht/Research Report PMS-FB-1998-13, September An Abstract Machine for Model Generation with PUHR Tableaux (Extended Abstract) Alexander von Drach, Tim Geisler, Sven Panne, and David Sacher Institut fur Informatik, Universitat Munchen, Oettingenstr. 67, D-80538 Munchen fvondrach---geisler---panne---sacherg@informatik.uni-muenchen.de 1 Introduction The model-generation paradigm for automated deduction [MB88] is to demonstrate the satisfiability of first-order formulas by constructing satisfying Herbrand interpretations (i. e., models) instead of demonstrating their unsatisfiability by constructing a refutation (e. g., a resolution proof). Model generation was originally motivated by database applications (a detai..