the proceedings contain 27 papers. the special focus in this conference is on logic for programming, artificialintelligence and reasoning. the topics include: Counterfactuals Modulo Temporal logics;an excursion to th...
the proceedings contain 27 papers. the special focus in this conference is on logic for programming, artificialintelligence and reasoning. the topics include: Counterfactuals Modulo Temporal logics;an excursion to the border of decidability: between two- and three-variable logic;a Mathematical Benchmark for Inductive theorem Provers;SMT Solving over Finite Field Arithmetic;overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification;A Fast and Accurate ASP Counting Based Network Reliability Estimator;collaborative Inference of Combined Invariants;Analyzing Multiple Conflicts in SAT: An Experimental Evaluation;An Interactive SMT Tactic in Coq using Abductive reasoning;Experiments on Infinite Model Finding in SMT Solving;embedding Intuitionistic into Classical logic;on the Complexity of Convex and Reverse Convex Prequadratic Constraints;representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order logic;Toward Optimal Radio Colorings of Hypercubes via SAT-solving;cartesian Reachability logic: A Language-Parametric logic for Verifying k-Safety Properties;scalable Probabilistic Routes;logic of Differentiable logics: Towards a Uniform Semantics of DL;model Checking Omega-Regular Hyperproperties with AutoHyperQ;refining Unification with Abstraction;Exploring Partial Models with SCL;trace-based Deductive Verification;How Much Should this Symbol Weigh? A GNN-Advised Clause Selection;guiding an Instantiation Prover with Graph Neural Networks;tighter Abstract Queries in Neural Network Verification.
In answer set programming, two groups of rules are considered strongly equivalent if they have the same meaning in any context. Strong equivalence of two programs can be sometimes established by deriving rules of each...
详细信息
ISBN:
(纸本)9783031742088;9783031742095
In answer set programming, two groups of rules are considered strongly equivalent if they have the same meaning in any context. Strong equivalence of two programs can be sometimes established by deriving rules of each program from rules of the other in an appropriate deductive system. this paper shows how to extend this method of proving strong equivalence to programs containing the counting aggregate.
Answer-set programming (ASP) is a declarative logicprogramming paradigm that provides an efficient problem-solving approach in logic-based artificialintelligence (AI). While it has proven successful, ASP encounters ...
详细信息
ISBN:
(纸本)9783031742088;9783031742095
Answer-set programming (ASP) is a declarative logicprogramming paradigm that provides an efficient problem-solving approach in logic-based artificialintelligence (AI). While it has proven successful, ASP encounters specific situations where its language falls short of accurately representing and reasoning about incomplete information. Researchers now widely agree that ASP requires powerful introspective reasoning withthe use of epistemic modal operators;yet, despite long-lasting debates on how to extend ASP with such operators, they cannot reach a consensus on satisfactory semantics. Cabalar et al. argue that such research should be grounded in formal robustness. thus, inspired by ASP's foundational properties, they introduce a structural principle called epistemic splitting and designate it as one of the compulsory criteria for epistemic ASP. this paper generalises their approach to a more comprehensive, meticulous, and conservative extension of ASP-splitting, thereby enhancing its applicability and efficiency.
ErgoAI (abbr. Ergo) is a high level, multi-paradigm logicprogramming language and system developed by Coherent Knowledge Systems as an enhancement of and a successor to the popular Flora-2 system. Ergo is oriented to...
详细信息
ISBN:
(纸本)9783031742088;9783031742095
ErgoAI (abbr. Ergo) is a high level, multi-paradigm logicprogramming language and system developed by Coherent Knowledge Systems as an enhancement of and a successor to the popular Flora-2 system. Ergo is oriented towards scalable knowledge representation and reasoning, and can exploit both structured knowledge as well as knowledge derived from external sources such as vector embeddings. From the start, Ergo (and Flora-2 before it) were designed to exploit the well-founded semantics for reasoning in a multi-paradigm environment, including object-based logic (F-logic) with non-monotonic inheritance;higher order syntax in the style of HiLog;defeasibility of rules;semantically clean transactional updates;and extensive use of subgoal delay for better logical behavior and performance. Although Ergo programs are compiled into XSB and adopt many Prolog features, Ergo is altogether a different language with functionality equivalent to major Prologs.
Connections of intuitionistic and intermediate logics withlogicprogramming have been extensively studied in the literature. Among the different results in the literature we find equilibrium logic (Pearce, 1996) and ...
详细信息
ISBN:
(纸本)9783031742088;9783031742095
Connections of intuitionistic and intermediate logics withlogicprogramming have been extensively studied in the literature. Among the different results in the literature we find equilibrium logic (Pearce, 1996) and Safe beliefs (Osorio et al., 2005). Pearce's approach admits a characterisation in terms of a fixpoint (consequence) operator on the here-and-there intermediate logic (Heyting, 1930), which is similar to the notion of theory completion in default and autoepistemic logics. Osorio's safe beliefs are also given in terms of a fixpoint operator under intuitionistic logic semantics. In this latter case, intuitionistic logic can be replaced by any intermediate logic without altering the result. In this paper we consider temporal equilibrium logic, an combination of equilibrium logic and linear-time temporal logic. In this context we extend Pearce's and Osorio's approach to temporal case and we discuss the relation of intuitionistic temporal logic and temporal logicprogramming.
We develop a computational approach to Metric Answer Set programming (ASP) to allow for expressing quantitative temporal constrains, like durations and deadlines. A central challenge is to maintain scalability when de...
ISBN:
(纸本)9783031742088;9783031742095
We develop a computational approach to Metric Answer Set programming (ASP) to allow for expressing quantitative temporal constrains, like durations and deadlines. A central challenge is to maintain scalability when dealing with fine-grained timing constraints, which can significantly exacerbate ASP's grounding bottleneck. To address this issue, we leverage extensions of ASP with difference constraints, a simplified form of linear constraints, to handle time-related aspects externally. Our approach effectively decouples metric ASP from the granularity of time, resulting in a solution that is unaffected by time precision.
Explainability in artificialintelligence (XAI) is crucial for enhancing the transparency and trustworthiness of AI systems. Our work focuses on providing clear explanations for why certain atoms in a given answer set...
详细信息
ISBN:
(纸本)9783031742088;9783031742095
Explainability in artificialintelligence (XAI) is crucial for enhancing the transparency and trustworthiness of AI systems. Our work focuses on providing clear explanations for why certain atoms in a given answer set are evaluated as such, hence contributing to the understanding of the decisions made by Answer Set programming (ASP) systems. We employ simple inference rules to elucidate these decisions, avoiding complex derivations to maintain clarity. Moreover, we introduce the notion of preferred unit-provable unsatisfiable subsets (preferred 1-PUS) to identify relevant portions of ASP encodings, prioritizing program rules over assignments, withthe objective of minimizing the assumptions involved in the explanation process. the proposed principles are implemented in a new XAI system.
Alternating-time Temporal logic (ATL) extends the temporal logic CTL, permitting quantification over coalitions of agents. During the model checking process, the coalitions defined in a given formula are predetermined...
详细信息
ISBN:
(纸本)9783031553257;9783031553264
Alternating-time Temporal logic (ATL) extends the temporal logic CTL, permitting quantification over coalitions of agents. During the model checking process, the coalitions defined in a given formula are predetermined, operating under the assumption that the user possesses knowledge about the specific coalitions under exam. However, this presumption is not universally applicable. the outcome of this paper is twofold. Initially, we introduce CATL, a modified version of ATL which empowers users to define coalition quantifiers based on two key attributes: the number of agents involved within the coalitions and the methodology for grouping these agents. Subsequently, we show the incorporation of CATL into MCMAS, a widely recognized tool dedicated to ATL model checking. Additionally, we provide details of this extension accompanied by empirical experiments.
Weather forecasting is important for saving lives, protecting property, and supporting economic activities. It provides timely warnings for severe weather, improves agricultural planning, and aids in disaster manageme...
详细信息
ISBN:
(纸本)9783031742088;9783031742095
Weather forecasting is important for saving lives, protecting property, and supporting economic activities. It provides timely warnings for severe weather, improves agricultural planning, and aids in disaster management. Neural networks and deep learning methods can achieve impressive accuracy in weather prediction, but their black-box nature lacks in explainability. To address this limitation, we investigated the potential of FastLAS, an Inductive logicprogramming (ILP) framework, to produce reliable and, more important, explainable weather predictions. FastLAS learns ASP programs whose syntax and structural semantics resemble natural human language, making them easily understandable and interpretable by humans. the supportedness of stable models allows a clear explanation of the predictions. Our empirical evaluation on data from an Italian weather forecasting center shows that our approach is capable of learning predictive models from small dataset (a few samples instead of the thousands needed by neural networks) achieving an accuracy higher than statistical machine learning base lines.
Inductive definitions are ubiquitous in mathematics and computer science, and play an important role in knowledge representation. To date, several proof systems have been developed for inductive definitions. However, ...
详细信息
ISBN:
(纸本)9783031742088;9783031742095
Inductive definitions are ubiquitous in mathematics and computer science, and play an important role in knowledge representation. To date, several proof systems have been developed for inductive definitions. However, these systems are typically limited to stratified definitions, while many important definitions are not stratified. Inspired by logicprogramming, the logic FO(ID) has been developed as an extension of classical first-order logic with general inductive definitions that go beyond stratification. this paper presents a classical sequent calculus LFO(ID) for FO(ID), based on the sequent calculus LKID by Brotherston and Simpson, which formalizes the principle of mathematical induction. While syntactically remaining close to LKID, LFO(ID) covers a substantially larger class of inductive definitions. the soundness of LFO(ID) is proven, thereby showing that a relatively conservative adaptation of LKID is capable of handling the liberal forms of definitions in FO(ID), governed by the intricate well-founded semantics.
暂无评论