First-Order Logic Theorem Proving and Model Building via Approximation and 
Instantiation

Teucke, Andreas; Weidenbach, Christoph

Datensatz

DATENSATZ AKTIONENEXPORT

Zur Ablage hinzufügen

Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben

Forschungspapier

First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation

MPG-Autoren

/persons/resource/persons127656

Teucke, Andreas
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons45719

Weidenbach, Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;

Externe Ressourcen

Es sind keine externen Ressourcen hinterlegt

Volltexte (beschränkter Zugriff)

Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.

Volltexte (frei zugänglich)

1503.02971v2
(Preprint), 230KB

Ergänzendes Material (frei zugänglich)

Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar

Zitation

Teucke, A., & Weidenbach, C. (2015). First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation. Retrieved from http://arxiv.org/abs/1503.02971.

Zitierlink: https://hdl.handle.net/11858/00-001M-0000-0025-694C-5

Zusammenfassung

Counterexample-guided abstraction refinement is a well-established technique in verification. In this paper we instantiate the idea for first-order logic theorem proving. Given a clause set $N$ we propose its abstraction into a clause set $N'$ belonging to a decidable first-order fragment. The abstraction preserves satisfiability: if $N'$ is satisfiable, so is $N$. A refutation in $N'$ can then either be lifted to a refutation in $N$, or it guides a refinement of $N$ and its abstraction $N'$ excluding the previously found refutation that is not liftable.