<script type="text/javascript">
<!--
document.write('<div id="oa_widget"></div>');
document.write('<script type="text/javascript" src="https://www.openaire.eu/index.php?option=com_openaire&view=widget&format=raw&projectId=undefined&type=result"></script>');
-->
</script>

COPY SCRIPT

For further information contact us at helpdesk@openaire.eu

Negation in logic programming

Name: Negation in logic programming
Creator: Kenneth Kunen
Keywords: Specification and verification (program logics, model checking, etc.), PROLOG, Logic, decidability, 0102 computer and information sciences, 02 engineering and technology, interpreters, 01 natural sciences, equational theory, logic programming

descriptionPublicationkeyboard_double_arrow_right Article 01 Dec 1987 English Publisher:Elsevier BVJournal:The Journal of Logic Programming, volume 4, pages 289-308 (issn: 0743-1066,

Authors: Kenneth Kunen;

doi: 10.1016/0743-1066(87)90007-0

Negation in logic programming

- Summary
- Subjects
- Metrics

Abstract

The most familiar approach to negation in logic programming is the closed data base (CDB) approach by K. Clark. It does not satisfy the author since it disagrees with most PROLOG interpreters even in some simple cases. A new semantics is proposed here which is a truncation of \textit{M. Fitting}'s [ibid. 2, 295-312 (1985; Zbl 0589.68011)] 3-valued semantics before the level w. This is proved to be recursively enumerable using decidability of (in fact quantifier elimination for) the equational theory CET which postulates axioms of unification (values of different functions are unequal, every function is 1-1, etc.). Equivalent definition is truth in all (not only Herbrand) 3-valued models of CET where equality is 2-valued. A lot of useful remarks is made.

Related Organizations

University of Wisconsin–Oshkosh
United States

Keywords

Specification and verification (program logics, model checking, etc.), PROLOG, Logic, decidability, interpreters, equational theory, logic programming, quantifier elimination, negation, 3-valued semantics, Abstract data types; algebraic specification, Theorem proving (deduction, resolution, etc.)

Impact byBIP!

	citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	324
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Top 10%
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Top 0.1%
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Top 10%