New directions in instantiation-based theorem proving

Harald Ganzinger; Konstantin Korovin

doi:10.1109/LICS.2003.1210045

New directions in instantiation-based theorem proving

Research output: Chapter in Book/Conference proceeding › Conference contribution

Abstract

We consider instantiation-based theorem proving whereby instances of clauses are generated by certain inferences, and where inconsistency is detected by propositional tests. We give a model construction proof of completeness by which restrictive inference systems as well as admissible simplification techniques can be justified. Another contribution of the paper are novel inference systems that allow one to also employ decision procedures for first-order fragments more complex than propositional logic. The decision procedure provides for an approximative consistency test, and the instance generation inference system is a means of successively refining the approximation.

Original language	English
Title of host publication	Proceedings - Symposium on Logic in Computer Science\|Proc Symp Logic Comput Sci
Pages	55-64
Number of pages	9
DOIs	https://doi.org/10.1109/LICS.2003.1210045
Publication status	Published - 2003
Event	18th Annual IEEE Symposium on Logic in Computer Science - Ottawa, Ont. Duration: 1 Jul 2003 → … http://ieeexplore.ieee.org/iel5/8592/27231/01210045.pdf?tp=&arnumber=1210045&isnumber=27231

Conference

Conference	18th Annual IEEE Symposium on Logic in Computer Science
City	Ottawa, Ont.
Period	1/07/03 → …
Internet address	http://ieeexplore.ieee.org/iel5/8592/27231/01210045.pdf?tp=&arnumber=1210045&isnumber=27231

Access to Document

10.1109/LICS.2003.1210045

Cite this

@inproceedings{4d5011dbae7e48d68d1ca727f11d521c,

title = "New directions in instantiation-based theorem proving",

abstract = "We consider instantiation-based theorem proving whereby instances of clauses are generated by certain inferences, and where inconsistency is detected by propositional tests. We give a model construction proof of completeness by which restrictive inference systems as well as admissible simplification techniques can be justified. Another contribution of the paper are novel inference systems that allow one to also employ decision procedures for first-order fragments more complex than propositional logic. The decision procedure provides for an approximative consistency test, and the instance generation inference system is a means of successively refining the approximation.",

author = "Harald Ganzinger and Konstantin Korovin",

year = "2003",

doi = "10.1109/LICS.2003.1210045",

language = "English",

pages = "55--64",

booktitle = "Proceedings - Symposium on Logic in Computer Science|Proc Symp Logic Comput Sci",

note = "18th Annual IEEE Symposium on Logic in Computer Science ; Conference date: 01-07-2003",

url = "http://ieeexplore.ieee.org/iel5/8592/27231/01210045.pdf?tp=&arnumber=1210045&isnumber=27231",

}

TY - GEN

T1 - New directions in instantiation-based theorem proving

AU - Ganzinger, Harald

AU - Korovin, Konstantin

PY - 2003

Y1 - 2003

N2 - We consider instantiation-based theorem proving whereby instances of clauses are generated by certain inferences, and where inconsistency is detected by propositional tests. We give a model construction proof of completeness by which restrictive inference systems as well as admissible simplification techniques can be justified. Another contribution of the paper are novel inference systems that allow one to also employ decision procedures for first-order fragments more complex than propositional logic. The decision procedure provides for an approximative consistency test, and the instance generation inference system is a means of successively refining the approximation.

AB - We consider instantiation-based theorem proving whereby instances of clauses are generated by certain inferences, and where inconsistency is detected by propositional tests. We give a model construction proof of completeness by which restrictive inference systems as well as admissible simplification techniques can be justified. Another contribution of the paper are novel inference systems that allow one to also employ decision procedures for first-order fragments more complex than propositional logic. The decision procedure provides for an approximative consistency test, and the instance generation inference system is a means of successively refining the approximation.

U2 - 10.1109/LICS.2003.1210045

DO - 10.1109/LICS.2003.1210045

M3 - Conference contribution

SP - 55

EP - 64

BT - Proceedings - Symposium on Logic in Computer Science|Proc Symp Logic Comput Sci

T2 - 18th Annual IEEE Symposium on Logic in Computer Science

Y2 - 1 July 2003

ER -

New directions in instantiation-based theorem proving

Abstract

Conference

Access to Document

Fingerprint

Cite this