A deduction method complete for refutation and finite satisfiability

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributedpeer-review

Contributors

Abstract

Database and Artificial Intelligence applications are briefly discussed and it is argued that they need deduction methods that are not only refutation complete but also complete for finite satisfiability. A novel deduction method is introduced for such applications. Instead of relying on Skolemization, as most refutation methods do, the proposed method processes existential quantifiers in a special manner which makes it complete not only for refutation, but also for finite satisfiability. A main contribution of this paper is the proof of these results.

Details

Original languageEnglish
Title of host publicationLogics in Artificial Intelligence
EditorsJurgen Dix, Luis Farinas del Cerro, Ulrich Furbach
PublisherSpringer Verlag
Pages122-138
Number of pages17
ISBN (print)3540651411, 9783540651413
Publication statusPublished - 1998
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science, Volume 1489
ISSN0302-9743

Conference

Title6th European Workshop on Logics in Artificial Intelligence
Abbreviated titleJELIA 1998
Conference number6
Duration12 - 15 October 1998
LocationSchloss Dagstuhl
CityWadern
CountryGermany

External IDs

ORCID /0000-0001-9756-6390/work/142250118

Keywords

Keywords

  • Artificial intelligence, Automated reasoning, Databases, Expert systems, Finite satisfiability

Library keywords