Computer Science – Programming Languages
Scientific paper
2000-05-08
Computer Science
Programming Languages
17 pages. Invited talk at the Computational Logic Conference (CL 2000). To appear in Springer-Verlag Lecture Notes in Computer
Scientific paper
In Apt and Bezem [AB99] (see cs.LO/9811017) we provided a computational interpretation of first-order formulas over arbitrary interpretations. Here we complement this work by introducing a denotational semantics for first-order logic. Additionally, by allowing an assignment of a non-ground term to a variable we introduce in this framework logical variables. The semantics combines a number of well-known ideas from the areas of semantics of imperative programming languages and logic programming. In the resulting computational view conjunction corresponds to sequential composition, disjunction to ``don't know'' nondeterminism, existential quantification to declaration of a local variable, and negation to the ``negation as finite failure'' rule. The soundness result shows correctness of the semantics with respect to the notion of truth. The proof resembles in some aspects the proof of the soundness of the SLDNF-resolution.
No associations
LandOfFree
A Denotational Semantics for First-Order Logic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with A Denotational Semantics for First-Order Logic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Denotational Semantics for First-Order Logic will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-425777