Source-linked AI summary
ASP-Core-2 Input Language Format
Francesco Calimeri, Wolfgang Faber, Martin Gebser, Giovambattista Ianni, Roland Kaminski, Thomas Krennwallner, Nicola Leone, Marco Maratea, Francesco Ricca, Torsten Schaub
TL;DR
ASP research needed a standardized solver input language to support shared competitions and solver development. The paper presents ASP-Core-2, extending ASP-Core with widely adopted constructs and defining its syntax, semantics, and practical restrictions. ASP-Core-2 has served as the standard language for ASP competitions since 2013, while recursive-aggregate semantics remains under consideration.
Problem
ASP requires a standardized solver input language to support common competition formats, solver development, and application of ASP methodology.
Method
The paper specifies ASP-Core-2 syntax and model-theoretic semantics, then gives expressive constructs and practical restrictions for admissible programs.
Results
ASP-Core-2 is the standard input language adopted by ASP solver competitions since 2013.
Takeaways & Limitations
ASP-Core-2 standardizes the language to which ASP solvers must adhere for participation in the ASP Competition series.
Takeaways & Limitations
Practical restrictions include non-recursive aggregates, and recursive-aggregate semantics is still under consideration.
Abstract
from arXiv · showhide
Standardization of solver input languages has been a main driver for the growth of several areas within knowledge representation and reasoning, fostering the exploitation in actual applications. In this document we present the ASP-Core-2 standard input language for Answer Set Programming, which has been adopted in ASP Competition events since 2013.
1 Introduction
ASP-Core-2 is the standardized input language for ASP solvers, extending earlier ASP-Core and adopted in ASP Competitions since 2013. Its standardization supports efficient solver development and broader academic and industrial use of ASP.
- Standard input languages have supported growth in knowledge representation and reasoning communities by enabling efficient solvers and solver competitions.
- ASP-Core originated as a restricted rule-based language extending the Core language to the non-ground case.
- ASP-Core-2 extends its predecessor with mature constructs including aggregates, weak constraints, and function symbols.
- ASP-Core-2 has been the standard input language adopted by ASP solver competitions since 2013.
- The competition series contributed to efficient ASP solvers and to academic and industrial exploitation of ASP methodology.
2 ASP-Core-2 Language Syntax
ASP-Core-2 specifies terms, atoms, literals, rules, weak constraints, queries, programs, and aggregates. Its syntax supports arithmetic and functional terms, optimization constructs, and aggregate collections, while allowing infinite aggregate collections for the stated ground-instantiation semantics.
- The specification uses mathematical notation and provides a lexical mapping to the raw input format.
- Terms: Terms may be constants, variables, arithmetic terms, or functional terms formed from a functor and one or more terms.
- Atoms and Naf-Literals: Predicate atoms use predicate names and terms, while built-in atoms compare terms and naf-literals include atoms or their default negations.
- Aggregate Literals: Aggregate atoms apply #count, #sum, #max, or #min to collections of aggregate elements and compare the result with a term.
- Aggregate Literals: Infinite aggregate-element collections are allowed because ground instantiation may produce infinitely many ground instances.
- Rules: Rules consist of disjunctive classical-atom heads and literal bodies; rules with empty bodies are facts, and rules with empty heads are constraints.
- Weak Constraints: Weak constraints associate literal bodies with weights and levels, with level 0 used when the optional level is omitted.
- Programs and Queries: An ASP-Core-2 program is a set of rules and weak constraints, optionally accompanied by one query, and objects are ground when they contain no variables.
3 Semantics
ASP-Core-2 gives a model-theoretic semantics based on ground instantiation, interpretations, satisfaction, reducts, and minimal models. It defines aggregate evaluation, optimal answer sets, and query truth, while restricting practical agreement to programs with non-recursive aggregates.
- Foundations: The semantics extends Herbrand interpretations to non-ground programs and accounts for integers as part of the Herbrand universe.
- Scope: The semantics is restricted to programs with non-recursive aggregates, for which it substantially agrees with several aggregate proposals.
- Ground Instantiation: Ground instantiation applies well-formed substitutions, expands aggregate elements, and arithmetically evaluates resulting ground rules, weak constraints, and queries.
- Satisfaction: Naf-literals and built-in atoms are evaluated relative to interpretations using a total order on terms.
- Aggregate Satisfaction: Aggregate evaluation first selects tuples whose associated naf-literals are true, then applies #count, #sum, #max, or #min and tests the aggregate relation.
- Answer Sets: An answer set is a subset-minimal model of the reduct formed by retaining ground rules whose bodies are true in the interpretation.
- Optimal Answer Sets: Optimal answer sets are selected from AS(P) by comparing weak-constraint violations across priority levels.
4 Syntactic Shortcuts
ASP-Core-2 defines syntactic shortcuts for anonymous variables, choice constructs, and aggregate relations, reducing them to the core language. These reductions preserve their intended generation and constraint behavior.
- Anonymous Variables: Anonymous-variable occurrences denote distinct fresh variables in each respective context.The underscore notation introduces a fresh variable independently at every occurrence.
- Choice Rules: Choice elements pair a classical atom with optional naf-literals, while choice atoms collect elements under an aggregate relation and bound.The relation and bound may be omitted in the default case of ≥ 0.
- Choice Rules: Choice rules are reduced to ordinary rules using fresh auxiliary predicate and function names that encode atom polarity.The first rule group generates admissible subsets, while an integrity constraint enforces the aggregate condition.
- Choice Rules: The reduction generates true or false choices when the body and element conditions hold, then requires the aggregate relation to be satisfied.For the illustration, at most one of p(a) and ¬p(a) can be selected under the ≤ 1 condition.
- Aggregate Relations: Aggregate relations support left and right notation, with combined expressions mapped to available constructs through specified transformations.The same shortcut mechanism applies to aggregate literals formed with or without negation as failure.
5 Using ASP-Core-2 in Practice – Restrictions
ASP-Core-2 imposes practical restrictions intended to support uncontroversial semantics, implementability, and finite competition inputs. These include safety, non-recursive aggregates, invariance under undefined arithmetic, and finiteness controls.
- Safety: Rules, weak constraints, and queries must be safe by binding all global and aggregate-local variables through permitted body conditions.Built-in and aggregate conditions impose additional binding requirements on variables appearing in arithmetic terms or aggregate elements.
- Finiteness: Competition inputs must satisfy finiteness requirements, enforced pragmatically through conditions or known maximum integer and function-nesting bounds.ASP Competitions adopt the bounds-based option, and programs such as p(X+1) ← p(X) can be inadmissible.
- Aggregates: Aggregates must be non-recursive, meaning aggregate dependencies cannot have a path from the aggregate predicate to the rule head predicate.The restriction is defined using a directed predicate dependency graph.
- Predicate Arities: Predicate arity is not fixed across atoms sharing a predicate name, although implementers are encouraged to warn about differing arities.The standard permits the situation but recommends diagnostic warnings.
- Undefined Arithmetics: Undefined arithmetic substitutions are excluded by ground instantiation but can cause implementation problems or unexpected behavior.Programs are therefore required to be invariant under undefined arithmetics, so arbitrary handling of undefined subterms does not change their semantics.
- Undefined Arithmetics: The example program with p(0). has answer set {a(0)} but can yield the wrong answer set {a(0), p} when a grounder skips arithmetic evaluation.This illustrates why invariance under undefined arithmetics is required.
6 EBNF Grammar and Lexical Table
The EBNF grammar specifies the concrete structure of ASP-Core-2 programs, including rules, weak constraints, queries, literals, choices, and aggregates. The lexical table defines tokens, comments, values, and operators used by the grammar.
- Program Structure: Programs consist of rule or weak-constraint statements, optionally followed by a query.The grammar represents heads, bodies, queries, and weak constraints through separate nonterminals.
- Rules and Aggregates: Bodies contain naf-literals or aggregates, while heads may be disjunctions or choice constructs.Choice and aggregate elements are comma- or semicolon-separated according to their grammatical productions.
- Rules and Aggregates: Aggregate functions include count, max, min, and sum, with aggregate elements formed from basic terms and optional naf-literals.The grammar uses braces and semicolons to delimit aggregate collections.
- Lexical Conventions: Comments and blank tokens may appear between tokens without syntactic or semantic meaning.Both single-line and multiline comment forms are listed in the lexical material.
7 Conclusions
The document presents ASP-Core-2 as the standardized language defining solver input syntax and semantics for ASP Competitions since 2013. Its evolution continues as the committee considers recursive aggregates and intermediate and output formats.
- Conclusions: The standardization committee continues evolving the language to remain aligned with developments in ASP research.Potential future work includes semantics for recursive aggregates and standards for intermediate and output formats.