In this paper we present a declarative approach to adding domain-dependent control knowledge for Answer Set Planning (ASP). Our approach allows different types of domain-dependent control knowledge such as hierarchica...
详细信息
the proceedings contain 19 papers. the special focus in this conference is on Verified Software: theories, Tools, and Experiments. the topics include: Constructing Independently Verifiable Privacy-Compliant Type Syste...
ISBN:
(纸本)9783030035914
the proceedings contain 19 papers. the special focus in this conference is on Verified Software: theories, Tools, and Experiments. the topics include: Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing Between Black-Box Components;sideTrail: Verifying Time-Balancing of Cryptosystems;towards Verification of Ethereum Smart Contracts: A Formalization of Core of Solidity;relational Equivalence Proofs Between Imperative and MapReduce Algorithms;practical Methods for reasoning About Java 8’s Functional programming Features;verification of Binarized Neural Networks via Inter-neuron Factoring: (Short Paper);the Map Equality Domain;loop Detection by logically Constrained Term Rewriting;store Buffer Reduction in the Presence of Mixed-Size Accesses and Misalignment;executable Counterexamples in Software Model Checking;Extending VIAP to Handle Array Programs;lattice-Based Refinement in Bounded Model Checking;verified Certificate Checking for Counting Votes;program Verification in the Presence of I/O: Semantics, Verified Library Routines, and Verified Applications;TWAM: A Certifying Abstract Machine for logic Programs;a Java Bytecode Formalisation;formalising Executable Specifications of Low-Level Systems.
the proceedings contain 11 papers. the topics discussed include: on model-theoretic strong normalization for truth-table natural deduction;extending equational monadic reasoning with monad transformers;towards a certi...
ISBN:
(纸本)9783959771825
the proceedings contain 11 papers. the topics discussed include: on model-theoretic strong normalization for truth-table natural deduction;extending equational monadic reasoning with monad transformers;towards a certified reference monitor of the android 10 permission system;coinductive proof search for polarized logic with applications to full intuitionistic propositional logic;synthetic completeness for a terminating Seligman-style tableau system;and two applications of logicprogramming to Coq.
Knowledge compilation converts Boolean formulae for which some inference tasks are computationally expensive into a representation where the same tasks are tractable. ProbLog is a state-of-the-art Probabilistic logic ...
详细信息
Encoding finite linear CSPs as Boolean formulas and solving them by using modern SAT solvers has proven to be highly effective by the award-winning sugar system. We here develop an alternative approach based on ASP th...
详细信息
In most works on negotiation dialogues, agents are supposed to be ideally honest. However, there are many situations where such a behaviour cannot always be expected from the agents (e.g. advertising, political negoti...
详细信息
Automated planning has been the subject of intensive research and is at the core of several areas of AI, including intelligent agents and robotics. In this thesis proposal, we argue that Concurrent Transaction logic (...
详细信息
Academia and industry are investigating novel approaches for processing vast amounts of data coming from enterprises, the Web, social media and sensor readings in an area that has come to be known as Big Data. logic p...
详细信息
ISBN:
(纸本)9781479965731
Academia and industry are investigating novel approaches for processing vast amounts of data coming from enterprises, the Web, social media and sensor readings in an area that has come to be known as Big Data. logicprogramming has traditionally focused on complex knowledge structures/programs. the question arises whether and how it can be applied in the context of Big Data. In this paper, we study how the well-founded semantics can be computed over huge amounts of data using mass parallelization. Specifically, we propose and evaluate a parallel approach based on the X10programming language. Our experiments demonstrate that our approach has the ability to process up to 1 billion facts within minutes.
the main contribution of this paper is the definition of the preference description language PDL. this language allows us to combine qualitative and quantitative, penalty based preferences in a flexible way. this make...
详细信息
暂无评论