Name
Abstract | ||
|---|---|---|
We consider instantiation-based theorem provingwhereby instances of clauses are generated by certaininferences, and where inconsistency is detected bypropositional tests. We give a model construction proofof completeness by which restrictive inference systemsas well as admissible simplification techniques can bejustified. Another contribution of the paper are novelinference systems that allow one to also employ decisionprocedures for first-order fragments more complex thanpropositional logic. The decision procedure provides for anapproximative consistency test, and the instance generationinference system is a means of successively refining theapproximation. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1109/LICS.2003.1210045 | LICS |
Keywords | Field | DocType |
approximation theory,inference mechanisms,theorem proving,approximation refinement,approximative consistency test,completeness proof,decision procedure,first-order fragment,instance generation,instantiation-based theorem proving,model construction,propositional logic,redundancy elimination,restrictive inference system,semantic selection,simplification technique | Discrete mathematics,Disjunction introduction,Second-order logic,Computer science,Inference,Automated theorem proving,Proof calculus,First-order logic,Proof complexity,Resolution (logic) | Conference |
ISSN | ISBN | Citations |
1043-6871 | 0-7695-1884-2 | 50 |
PageRank | References | Authors |
1.81 | 19 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Harald Ganzinger | 1 | 1513 | 155.21 |
| Konstantin Korovin | 2 | 288 | 20.64 |