the proceedings contain 6 papers. the topics discussed include: cylindrical algebraic coverings for quantifiers;SMT-solving induction proofs of inequalities;decidability of difference logics with unary predicates;auto...
the proceedings contain 6 papers. the topics discussed include: cylindrical algebraic coverings for quantifiers;SMT-solving induction proofs of inequalities;decidability of difference logics with unary predicates;automatic deployment of component-based applications in the cloud;enumerating projective planes of order nine with proof verification;and an SC-square approach to the minimum Kochen–Specker problem.
the proceedings contain 7 papers. the topics discussed include: care robots learning rules of ethical behavior under the supervision of an ethical teacher;a parallelization approach for hybrid-AI-based models: an appl...
the proceedings contain 7 papers. the topics discussed include: care robots learning rules of ethical behavior under the supervision of an ethical teacher;a parallelization approach for hybrid-AI-based models: an application study for semantic segmentation of medical images;towards inductive learning of domain-specific heuristics for ASP;mining sequences in phone recordings with answer set programming;estimation-based verification of cyber-physical systems via statistical model checking;explainability via short formulas: the case of propositional logic with implementation;and evaluating epistemic logic programs via answer set programming with quantifiers.
Matching logic is the foundation of the K semantic environment for the specification of programming languages and automated generation of evaluators and verification tools. NLML is a formalization of nominal logic, wh...
详细信息
ISBN:
(纸本)9798400713477
Matching logic is the foundation of the K semantic environment for the specification of programming languages and automated generation of evaluators and verification tools. NLML is a formalization of nominal logic, which facilitates specification and reasoning about languages with binders, as a matching logictheory. Many properties of interest are inductive, and to prove them an induction principle modulo alpha-equality is required. In this paper we show that an alpha-structural Induction Principle for any nominal binding signature can be derived in an extension of NLML with set variables and fixpoint operators. We illustrate the use of the principle to prove properties of the lambda-calculus, the computation model underlying functional programming languages. the techniques generalize to other languages with binders. the proofs have been written in and generated using Metamath Zero.
Petri nets are a class of models of computation used to compactly represent discrete event systems. Among many application domains, they have now become the most prominent formalism to express process models in Proces...
详细信息
ISBN:
(纸本)9783031742088;9783031742095
Petri nets are a class of models of computation used to compactly represent discrete event systems. Among many application domains, they have now become the most prominent formalism to express process models in Process Mining, thanks to their formal semantics that enables automated analysis techniques. In this context, model repair is the task of aligning a process model with actual executions of the process. Current solutions to model repair do not allow for embedding domain knowledge, providing guarantees of rigor, and enforcing structural requirements at the same time. In this paper, we fill this gap by proposing an approach based on the Inductive logicprogramming system ILASP. We then implement our approach and perform an experimental evaluation, showing both its expressiveness and feasibility.
this paper presents a software module for working with fuzzy logic inference systems in the context of fuzzy case-based reasoning. Fuzzy logic, providing tools for describing and handling uncertainty, is an important ...
详细信息
We show a projective Beth definability theorem for logic programs under the stable model semantics: For given programs P and Q and vocabulary V (set of predicates) the existence of a program R in V such that P. R and ...
详细信息
ISBN:
(数字)9783031634987
ISBN:
(纸本)9783031634970;9783031634987
We show a projective Beth definability theorem for logic programs under the stable model semantics: For given programs P and Q and vocabulary V (set of predicates) the existence of a program R in V such that P. R and P. Q are strongly equivalent can be expressed as a first-order entailment. Moreover, our result is effective: A program R can be constructed from a Craig interpolant for this entailment, using a known first-order encoding for testing strong equivalence, which we apply in reverse to extract programs from formulas. As a further perspective, this allows transforming logic programs via transforming their first-order encodings. In a prototypical implementation, the Craig interpolation is performed by first-order provers based on clausal tableaux or resolution calculi. Our work shows how definability and interpolation, which underlie modern logic-based approaches to advanced tasks in knowledge representation, transfer to answer set programming.
We automate deep step-by step reasoning in an LLM dialog thread by recursively exploring alternatives (OR-nodes) and expanding details (AND-nodes) up to a given depth. Starting from a single succinct task-specific ini...
详细信息
ISBN:
(纸本)9789819722990;9789819723003
We automate deep step-by step reasoning in an LLM dialog thread by recursively exploring alternatives (OR-nodes) and expanding details (AND-nodes) up to a given depth. Starting from a single succinct task-specific initiator we steer the automated dialog thread to stay focussed on the task by synthesizing a prompt that summarizes the depth-first steps taken so far. Our algorithm is derived from a simple recursive descent implementation of a Horn Clause interpreter, except that we accommodate our logic engine to fit the natural language reasoning patterns LLMs have been trained on. Semantic similarity to ground-truth facts or oracle advice from another LLM instance is used to restrict the search space and validate the traces of justification steps returned as focussed and trustable answers. At the end, the unique minimal model of a generated Horn Clause program collects the results of the reasoning process. As applications, we sketch implementations of consequence predictions, causal explanations, recommendation systems and topic-focussed exploration of scientific literature.
Don’t Starve is a survival video game where the objective is for the player to survive as long as possible without dying. the game is challenging to play due to new situations being randomly generated making survival...
详细信息
Symbolic execution is a way of modelling the program state without executing it. It can be used to reason about the behaviour of the program statically. One of the use cases for using symbolic execution is finding sof...
详细信息
ISBN:
(纸本)9798350386608;9798350386592
Symbolic execution is a way of modelling the program state without executing it. It can be used to reason about the behaviour of the program statically. One of the use cases for using symbolic execution is finding software bugs. Clang Static Analyzer can perform static analysis using symbolic execution, and the specific problems to detect are described in imperative C++ code. One of the alternative ways of describing software bugs is linear temporal logic. this approach leads to a declarative description of the problem and allows for a higher level of abstraction. We present a mapping between the declarative temporal logic approach and the imperative Clang Static Analyzer implementation, highlighting the semantic equivalences of temporal logical formulas and C++ programs explicitly focusing on finding bugs statically. We briefly show the implementation details of our extension and present how to use temporal logic for symbolic execution in a powerful manner.
暂无评论