Declarative modeling of the operational behavior of logic languages
A new declarative semantics for logic programs is introduced and investigated. This new semantics differs essentially from the standard van Emden-Kowalsky semantics for logic programs, allowing the presence of atoms with variables in interpretations. The latter gives possibility to model the truth of universal formulae directly and to prove a more elegant completeness theorem than the standard one. Two types of new semantics based on upwards closure and subset properties imposed on sets of atoms in interpretations are studied and compared. It is proved that both types of interpretations form complete lattices. These new semantics are shown to capture the difference between effectively computable answers and answers obtainable by instantiations of universally quantified variables. As the authors argue, this fills the gap between operational and declarative semantics existing in the standard semantics for logic programs. Counterparts of results on classical Herbrand model semantics, including existence of minimal models, fixpoint characterization, etc., are shown to hold for the new semantics. Also, a stronger versions of soundness and completeness theorems for SLD-resolution are proved. Guidelines for future research, including characterization of finite failure sets, the description of semantics for logical programs with negation and universally quantified atoms are sketched.
- A fixpoint semantics of Horn sentences based on substitution sets
- Contributions to the Theory of Logic Programming
- Error diagnosis in logic programming an adaptation of E.Y. Shapiro's method
- scientific article; zbMATH DE number 3872640 (Why is no real title available?)
- scientific article; zbMATH DE number 3945331 (Why is no real title available?)
- scientific article; zbMATH DE number 4037276 (Why is no real title available?)
- The Semantics of Predicate Logic as a Programming Language
- Toward a declarative semantics for infinite objects in logic programming
- Unit Refutations and Horn Sets
- S-semantics for logic programming: a retrospective look
- Abstract interpretation of resolution-based semantics
- Semantic models for concurrent logic languages
- From failure to success: Comparing a denotational and a declarative semantics for Horn clause logic
- Unfolding and fixpoint semantics of concurrent constraint logic programs
- Compositionality properties of SLD-derivations
- Transforming constraint logic programs
- Uniform closures: Order-theoretically reconstructing logic program semantics and abstract domain refinements
- The reduced relative power operation on abstract domains
- A compositional semantics for logic programs
- A denotational semantics and dataflow construction for logic programs
- Bottom-up abstract interpretation of logic programs
- Deriving fold/unfold transformations of logic programs using extended OLDT-based abstract interpretation
- A declarative approach for first-order built-in's of Prolog
- SLDNF resolution with non-safe rule and fixpoint semantics for general logic programs
- Constraint logic programming with dynamic scheduling: A semantics based on closure operators
- Institutions for logic programming
- Constrained dependencies
- A new framework for declarative programming
- Type dependencies for logic programs using ACI-unification
- A model-theoretic reconstruction of the operational semantics of logic programs
- An abstract interpretation framework to reason on finite failure and other properties of finite and infinite computations.
- A theory of observables for logic programs
- On computability by logic programs
- The powerset operator on abstract interpretations
- Fast offline partial evaluation of logic programs
- Declarative debugging of functional logic programs
- A debugging scheme for functional logic programs
- Logic Foundations of the OCL Modelling Language
- Coalgebraic semantics for parallel derivation strategies in logic programming
- scientific article; zbMATH DE number 4180815 (Why is no real title available?)
- scientific article; zbMATH DE number 823595 (Why is no real title available?)
- scientific article; zbMATH DE number 936829 (Why is no real title available?)
- Description, implementation, and evaluation of a generic design for tabled CLP
- Unfolding and fixpoint semantics of concurrent constraint logic programs
- Algebraic methods in the compositional analysis of logic programs
- An integrated framework for the diagnosis and correction of rule-based programs
- On Correctness and Completeness of an n Queens Program
- S-semantics -- an example
- Nondeterminism and infinite computations in constraint programming
- Fully abstract compositional semantics for an algebra of logic programs
- Efficient bottom-up execution of logic programs using abstract interpretation
- Is there an axiomatic semantics for standard pure Prolog?
- Comparative semantics for flow of control in logic programming without logic
- Reactive systems, (semi-)saturated semantics and coalgebras on presheaves
- A new generic scheme for functional logic programming with constraints
- Finite failures and partial computations in concurrent logic languages
- A declarative semantics of flat guarded Horn clauses for programs with perpetual processes
- A compact fixpoint semantics for term rewriting systems
This page was built for publication: Declarative modeling of the operational behavior of logic languages
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q913530)
