ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Fourth Annual IEEE Symposium on

Logic in Computer Science (LICS 1989)

Paper: Negation as refutation (at LICS 1989)

Authors: Melvin Fitting


A refutation mechanism is introduced into logic programming, dual to the usual proof mechanism; then negation is treated via refutation. A four-valued logic is appropriate for the semantics: true, false, neither, both. Inconsistent programs are allowed, but inconsistencies remain localized. The four-valued logic is a well-known one, due to Belnap, and is the simplest example of the Ginsberg bilattice notion. An efficient implementation based on semantic tableaux is sketched; it reduces to SLD resolution when negations are not involved. The resulting system can give reasonable answers to queries that involve both negation and free variables. Also, it gives the same results as Prolog when there are no negations. Finally, an implementation in Prolog is given


    author = 	 {Melvin Fitting},
    title = 	 {Negation as refutation},
    booktitle =  {Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 1989)},
    year =	 {1989},
    month =	 {June}, 
    pages =      {63--70},
    location =   {Pacific Grove, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}

Last modified: 2022-10-3113:49
Sam Staton