Paper Info
Title
A logic programming and verification system for recursive quantificational logic
Abstract
In this paper, we describe a logic programming and program verification system which is based on quantifier elimination techniques and axiomatization rather than on more common method of doing logic programming using the Herbrand-Prawitz-Robinson unification algorithm without occur-check. This system is shown to have interesting properties for logic programming and includes a number of advanced features. Among these features are user-defined data objects, user-defined recursive relations and functions, either of which may involve quantifiers in the body of their definitions, and automatic termination and consistency checking for recursively defined concept. In addition, it has a correct implementation of negation in contrast to PROLOG implementation of negation as failure, a smooth interaction between LISP-like functions and PROLOG-like relations, and a smooth interaction between specifications and programs. Finally, it provides a method of mathematical induction applicable to recursive definitions involving quantifiers.
Year
Venue
Keywords
1985
IJCAI
user-defined data object,lisp-like function,herbrand-prawitz-robinson unification algorithm,program verification system,user-defined recursive relation,logic programming,recursive quantificational logic,prolog implementation,smooth interaction,correct implementation,common method,computational logic,quantifier elimination
Field
DocType
ISBN
Functional logic programming,Discrete mathematics,Horn clause,Programming language,Computer science,Inductive programming,Zeroth-order logic,Prolog,Logic programming,Predicate logic,Higher-order logic
Conference
0-934613-02-8
Citations 
PageRank 
References 
4
0.66
4
Authors
2
Name
Order
Citations
PageRank
Frank M. Brown13914.50
Peiya Liu250235.42