Paper Info
Title
A Logic for Nondeterministic Functional Programs (Extended Abstract)
Abstract
We present a schematic functional programming language coupled with a logic of programs. Our language allows for -recursion, -abstraction, nondeterminism and calls to predefined functions. We define a denotational semantics, show that Kozen's propositional -calculus and Harel's first order dynamic logic for regular programs can be embedded in our logic LRF, and establish the soundness and completeness of two different proof systems: one using infinitary rules and an arithmetically complete one.
Year
DOI
Venue
1989
10.1007/3-540-51498-8_19
FCT
Keywords
Field
DocType
extended abstract,nondeterministic functional programs,functional programming language,functional programming,first order,dynamic logic
Functional logic programming,Horn clause,Programming language,Computer science,Description logic,Theoretical computer science,Prolog,Logic programming,Soundness,Dynamic logic (digital electronics),Dynamic logic (modal logic)
Conference
ISBN
Citations 
PageRank 
3-540-51498-8
0
0.34
References 
Authors
7
1
Name
Order
Citations
PageRank
Ana Gil-Luezas1302.95