Disjunctive ASP with functions: decidable queries and effective computation
From MaRDI portal
Publication:3585164
Abstract: Querying over disjunctive ASP with functions is a highly undecidable task in general. In this paper we focus on disjunctive logic programs with stratified negation and functions under the stable model semantics (ASP^{fs}). We show that query answering in this setting is decidable, if the query is finitely recursive (ASP^{fs}_{fr}). Our proof yields also an effective method for query evaluation. It is done by extending the magic set technique to ASP^{fs}_{fr}. We show that the magic-set rewritten program is query equivalent to the original one (under both brave and cautious reasoning). Moreover, we prove that the rewritten program is also finitely ground, implying that it is decidable. Importantly, finitely ground programs are evaluable using existing ASP solvers, making the class of ASP^{fs}_{fr} queries usable in practice.
Recommendations
- Finitely recursive programs: decidability and bottom-up computation
- Magic Sets for the Bottom-Up Evaluation of Finitely Recursive Programs
- scientific article; zbMATH DE number 6139984
- Computable Functions in ASP: Theory and Implementation
- $\mathbb{FDNC}$ : Decidable Non-monotonic Disjunctive Logic Programs with Function Symbols
Cites work
- $\mathbb{FDNC}$ : Decidable Non-monotonic Disjunctive Logic Programs with Function Symbols
- Bottom-up evaluation and query optimization of well-founded models
- Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation
- Horn clause computability
- Magic Sets for the Bottom-Up Evaluation of Finitely Recursive Programs
- On finitely recursive programs
- On the power of magic
- Reasoning with infinite stable models
Cited in
(11)- Finitely recursive programs: decidability and bottom-up computation
- Terminating evaluation of logic programs with finite three-valued models
- Magic Sets for the Bottom-Up Evaluation of Finitely Recursive Programs
- Cautious reasoning in ASP via minimal models and unsatisfiable cores
- Checking termination of bottom-up evaluation of logic programs with function symbols
- Using linear constraints for logic program termination analysis
- {\textsc{ASPeRiX}}, a first-order forward chaining approach for answer set computing
- ASP with non-herbrand partial functions: a language and system for practical use
- Logic programming with function symbols: checking termination of bottom-up evaluation through program adornments
- Computable Functions in ASP: Theory and Implementation
- Abstraction for non-ground answer set programs
This page was built for publication: Disjunctive ASP with functions: decidable queries and effective computation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3585164)