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

Teucke, Andreas; Weidenbach, Christoph

Item

ITEM ACTIONSEXPORT

Add to Basket

Please note that a newer version of this item is available:
https://pure.mpg.de/pubman/item/item_2110994_5

DetailsSummary

Released

Paper

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

MPS-Authors

/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;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

1503.02971v2
(Preprint), 230KB

Supplementary Material (public)

There is no public supplementary material available

Citation

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.

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

Abstract

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.