Implementation of Constructive Negation in Extensional Higher-Order Logic Programming

Graduate Thesis uoadl:1692144 904 Read counter

Unit:
Department of Informatics and Telecommunications
Πληροφορική
Deposit date:
2017-06-29
Year:
2017
Author:
Dona Ergys
Supervisors info:
Πάνος Ροντογιάννης, Καθηγητής, Πληροφορικής και Τηλεπικοινωνιών, ΕΚΠΑ
Άγγελος Χαραλαμπίδης, Ερευνητής, ΕΚΕΦΕ «Δημόκριτος»
Original Title:
Implementation of Constructive Negation in Extensional Higher-Order Logic Programming
Languages:
English
Translated title:
Implementation of Constructive Negation in Extensional Higher-Order Logic Programming
Summary:
Constructive negation is a logic programming negation method that allows the handling of non-ground negative literals. Logic programming systems which are enhanced with constructive negation may produce not only equalities (assignments or unifications of variables), but also inequalities, that, roughly speaking, restrict variables to be different from some value.

Extensional higher-order logic programming is a logic programming paradigm that extends classical (first-order) logic programming by introducing higher-order terms, while preserving all the well-known properties of the former. These higher-order terms (variables) represent sets, which contain elements for which the former succeed.

An extensional higher-order logic programming language called HOPES has been recently proposed. HOPES has been enhanced with constructive negation to create "HOPES with constructive negation".

While the foundations of HOPES are based on strong and well-defined semantics, implementing a logic programming system (interpreter) for it proved to be a real challenge. The reason is that the enhanced definition of the HOPES proof procedure does not define any particular method for selecting the next subgoal to be satisfied. We show that, while the language definition guarantees that there exist paths in the proof tree that lead to correct answers, if a naive selection policy (e.g. always selecting the left-most literal, like PROLOG does) is adopted, then one has to take extra measures in order to avoid following paths that will never lead to correct solutions.

The contribution of this thesis consists of the redefinition of some of the rules in the HOPES proof procedure. We show that the redefined proof procedure allows the implementation of an interpreter for HOPES, which follows the left-most derivation rule of PROLOG and behaves correctly (only gives correct answers) for any given query.
Main subject category:
Computer science
Keywords:
logic, programming, negation, high-order, extensional
Index:
Yes
Number of index pages:
2
Contains images:
Yes
Number of references:
8
Number of pages:
48
e.dona_bsc_thesis.pdf (318 KB) Open in new window

 


hopes-cn_restrict.zip
90 KB
File access is restricted.