Well-founded semantics

Last updated

In computer science, the well-founded semantics is a three-valued semantics for logic programming, which gives a precise meaning to general logic programs.

Contents

History

The well-founded semantics was defined by Van Gelder, et al. in 1988. [1] [2] The Prolog system XSB implements the well-founded semantics since 1997. [3] [4]

Three-valued logic

The well-founded semantics assigns a unique model to every general logic program. However, instead of only assigning propositions true or false, it adds a third value unknown for representing ignorance. [1]

A simple example is the logic program that encodes two propositions a and b, and in which a must be true whenever b is not and vice versa:

a:-not(b).b:-not(a).

neither a nor b are true or false, but both have the truth value unknown. In the two-valued stable model semantics, there are two stable models, one in which a is true and b is false, and one in which b is true and a is false.

Stratified logic programs have a 2-valued well-founded model, in which every proposition is either true or false. This coincides with the unique stable model of the program. The well-founded semantics can be viewed as a three-valued version of the stable model semantics. [5]

Complexity

In 1989, Van Gelder suggested an algorithm to compute the well-founded semantics of a propositional logic program whose time complexity is quadratic in the size of the program. [6] As of 2001, no general subquadratic algorithm for the problem was known. [7]

Related Research Articles

Logic programming is a programming, database and knowledge-representation and reasoning paradigm which is based on formal logic. A program, database or knowledge base in a logic programming language is a set of sentences in logical form, expressing facts and rules about some problem domain. Major logic programming language families include Prolog, Answer Set Programming (ASP) and Datalog. In all of these languages, rules are written in the form of clauses:

Prolog is a logic programming language associated with artificial intelligence and computational linguistics.

In computer science, declarative programming is a programming paradigm—a style of building the structure and elements of computer programs—that expresses the logic of a computation without describing its control flow.

In mathematical logic and logic programming, a Horn clause is a logical formula of a particular rule-like form that gives it useful properties for use in logic programming, formal specification, universal algebra and model theory. Horn clauses are named for the logician Alfred Horn, who first pointed out their significance in 1951.

Bunched logic is a variety of substructural logic proposed by Peter O'Hearn and David Pym. Bunched logic provides primitives for reasoning about resource composition, which aid in the compositional analysis of computer and other systems. It has category-theoretic and truth-functional semantics, which can be understood in terms of an abstract concept of resource, and a proof theory in which the contexts Γ in an entailment judgement Γ ⊢ A are tree-like structures (bunches) rather than lists or (multi)sets as in most proof calculi. Bunched logic has an associated type theory, and its first application was in providing a way to control the aliasing and other forms of interference in imperative programs. The logic has seen further applications in program verification, where it is the basis of the assertion language of separation logic, and in systems modelling, where it provides a way to decompose the resources used by components of a system.

Datalog is a declarative logic programming language. While it is syntactically a subset of Prolog, Datalog generally uses a bottom-up rather than top-down evaluation model. This difference yields significantly different behavior and properties from Prolog. It is often used as a query language for deductive databases. Datalog has been applied to problems in data integration, networking, program analysis, and more.

In computational complexity theory, a nonelementary problem is a problem that is not a member of the class ELEMENTARY. As a class it is sometimes denoted as NONELEMENTARY.

Answer set programming (ASP) is a form of declarative programming oriented towards difficult search problems. It is based on the stable model semantics of logic programming. In ASP, search problems are reduced to computing stable models, and answer set solvers—programs for generating stable models—are used to perform search. The computational process employed in the design of many answer set solvers is an enhancement of the DPLL algorithm and, in principle, it always terminates.

Negation as failure is a non-monotonic inference rule in logic programming, used to derive from failure to derive . Note that can be different from the statement of the logical negation of , depending on the completeness of the inference algorithm and thus also on the formal logic system.

The autoepistemic logic is a formal logic for the representation and reasoning of knowledge about knowledge. While propositional logic can only express facts, autoepistemic logic can express knowledge and lack of knowledge about facts.

The concept of a stable model, or answer set, is used to define a declarative semantics for logic programs with negation as failure. This is one of several standard approaches to the meaning of negation in logic programming, along with program completion and the well-founded semantics. The stable model semantics is the basis of answer set programming.

XSB is the name of a dialect of the Prolog programming language and its implementation developed at Stony Brook University in collaboration with the Katholieke Universiteit Leuven, the New University of Lisbon, Uppsala University and software vendor XSB, Inc.

F-logic is a knowledge representation and ontology language. F-logic combines the advantages of conceptual modeling with object-oriented, frame-based languages and offers a declarative, compact and simple syntax, as well as the well-defined semantics of a logic-based language.

M. Dale Skeen is an American computer scientist. He specializes in designing and implementing large-scale computing systems, distributed computing and database management systems.

The following Comparison of Prolog implementations provides a reference for the relative feature sets and performance of different implementations of the Prolog computer programming language.

<span class="mw-page-title-main">Georg Gottlob</span> Austrian computer scientist

Georg Gottlob FRS is an Austrian-Italian computer scientist who works in the areas of database theory, logic, and artificial intelligence and is Professor of Informatics at the University of Calabria. He was Professor at the University of Oxford.

<span class="mw-page-title-main">Tomasz Imieliński</span> Polish-American computer scientist (born 1954)

Tomasz Imieliński is a Polish-American computer scientist, most known in the areas of data mining, mobile computing, data extraction, and search engine technology. He is currently a professor of computer science at Rutgers University in New Jersey, United States.

In database theory, Imieliński–Lipski algebra is an extension of relational algebra onto tables with different types of null values. It is used to operate on relations with incomplete information.

Logic programming is a programming paradigm that includes languages based on formal logic, including Datalog and Prolog. This article describes the syntax and semantics of the purely declarative subset of these languages. Confusingly, the name "logic programming" also refers to a specific programming language that roughly corresponds to the declarative subset of Prolog. Unfortunately, the term must be used in both senses in this article.

Tabling is a technique first developed for natural language processing, where it was called Earley parsing. It consists of storing in a table partial successful analyses that might come in handy for future reuse.

References

  1. 1 2 Van Gelder, Allen; Ross, Kenneth A.; Schlipf, John S. (July 1991). "The well-founded semantics for general logic programs". Journal of the ACM. 38 (3): 619–649. doi:10.1145/116825.116838. ISSN   0004-5411.
  2. ↑ Van Gelder, Allen; Ross, Kenneth; Schlipf, John S. (1988). "Unfounded sets and well-founded semantics for general logic programs". Proceedings of the seventh ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems - PODS '88. New York, New York, USA: ACM Press. doi: 10.1145/308386.308444 .
  3. ↑ Körner, Philipp; Leuschel, Michael; Barbosa, João; Costa, Vítor Santos; Dahl, Verónica; Hermenegildo, Manuel V.; Morales, Jose F.; Wielemaker, Jan; Diaz, Daniel; Abreu, Salvador; Ciatto, Giovanni (November 2022). "Fifty Years of Prolog and Beyond". Theory and Practice of Logic Programming. 22 (6): 776–858. doi: 10.1017/S1471068422000102 . ISSN   1471-0684.
  4. ↑ Rao, Prasad; Sagonas, Konstantinos; Swift, Terrance; Warren, David S.; Freire, Juliana (1997), Dix, Jürgen; Furbach, Ulrich; Nerode, Anil (eds.), "XSB: A system for efficiently computing well-founded semantics", Logic Programming And Nonmonotonic Reasoning, Berlin, Heidelberg: Springer Berlin Heidelberg, vol. 1265, pp. 430–440, doi:10.1007/3-540-63255-7_33, ISBN   978-3-540-63255-9 , retrieved 2023-11-17
  5. ↑ Przymusinski, Teodor. Well-founded Semantics Coincides with Three-Valued Stable Semantics . Fundamenta Informaticae XIII pp. 445-463, 1990.
  6. ↑ Van Gelder, A. (1989). The alternating fixpoint of logic programs with negation. Proceedings of the eighth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems. ACM Press. pp. 1–10. doi: 10.1145/73721.73722 . ISBN   978-0-89791-308-9.
  7. ↑ Lonc, Zbigniew; Truszczyński, Mirosław (2001). "On the problem of computing the well-founded semantics". Theory and Practice of Logic Programming. 1 (5): 591–609. arXiv: cs/0101014 . doi:10.1017/S1471068401001053. ISSN   1471-0684.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.