the θ-subsumption test is known to be a bottleneck in inductivelogicprogramming. the state-of-the-art learning systems in this field are hardly scalable. Last year, we have created a distributed θ-subsumption proc...
详细信息
the θ-subsumption test is known to be a bottleneck in inductivelogicprogramming. the state-of-the-art learning systems in this field are hardly scalable. Last year, we have created a distributed θ-subsumption process based on an Actor Model, withthe aim of being able to decide subsumption on very large clauses. this model was correct and complete, but was also very slow. this is why we introduce ANTS (Actor Network based theta-Subsumption), a new model also based on an actor network, which is significantly faster than the previous one.
the proceedings contain 61 papers. the special focus in this conference is on Computer Aided Verification. the topics include: Verified compilation of space-efficient reversible circuits;ascertaining uncertainty for e...
ISBN:
(纸本)9783319633893
the proceedings contain 61 papers. the special focus in this conference is on Computer Aided Verification. the topics include: Verified compilation of space-efficient reversible circuits;ascertaining uncertainty for efficient exact cache analysis;non-polynomial worst-case analysis of recursive programs;decorated-component-based program synthesis;electrical bug localization during post-silicon validation enabled by quick error detection and formal methods;efficient parallel strategy improvement for parity games;model-checking linear-time properties of parametrized asynchronous shared memory pushdown systems;minimization of symbolic transducers;abstract interpretation with unfoldings;cutoff bounds for consensus algorithms;towards verifying nonlinear integer arithmetic;network-wide configuration synthesis;verifying equivalence of spark programs;synchronization synthesis for network programs;an experimentation framework for bounded synthesis;quantitative assume guarantee synthesis;syntax-guided optimal synthesis for chemical reaction networks;model counting for recursively-defined strings;a three-tier strategy for reasoning about floating-point numbers in SMT;a correct-by-decision solution for simultaneous place and route;on expansion and resolution in CEGAR based QBF solving;a decidable fragment in separation logic withinductive predicates and arithmetic;finding fix locations for CFL reachability analyses via minimum cuts;proving linearizability using forward simulations;automating induction for solving horn clauses and on multiphase-linear ranking functions.
this paper develops a probabilistic-epistemic logic program language, PELP, by introducing probabilistic modal operators K w and PL into LP MLN programs, where w is a sub-interval of [0, 1]. Intuitively, a probabili...
详细信息
this paper develops a probabilistic-epistemic logic program language, PELP, by introducing probabilistic modal operators K w and PL into LP MLN programs, where w is a sub-interval of [0, 1]. Intuitively, a probabilistic epistemic literal K w e denotes that e is known with a probability in w, and a probabilistic comparing literal PL(e 1 , e 2 ) denotes it is known that the probability of e 1 is less than the one of e 2 . the semantics of the new language is based on the semantics of LP MLN and epistemic specifications. In this paper, we analyze the relationship between PELP and some other epistemic logicprogramming languages. We also propose an algorithm for solving PELP programs, and then investigate the application of PELP for modeling and solving the Monty Hall problem and a conformant planning problem with a threshold.
the multi-agent pathfinding (MAPF) problem has attracted considerable attention because of its relation to practical applications. In this paper, we present a constraint-based declarative model for MAPF, together with...
详细信息
the multi-agent pathfinding (MAPF) problem has attracted considerable attention because of its relation to practical applications. In this paper, we present a constraint-based declarative model for MAPF, together with its implementation in Picat, a logic-based programming language. We show experimentally that our Picat-based implementation is highly competitive and sometimes outperforms previous approaches. Importantly, the proposed Picat implementation is very versatile. We demonstrate this by showing how it can be easily adapted to optimize different MAPF objectives, such as minimizing makespan or minimizing the sum of costs, and for a range of MAPF variants. Moreover, a Picat-based model can be automatically compiled to several general-purpose solvers such as SAT solvers and Mixed Integer programming solvers (MIP). this is particularly important for MAPF because some MAPF variants are solved more efficiently when compiled to SAT while other variants are solved more efficiently when compiled to MIP. We analyze these differences and the impact of different declarative models and encodings on empirical performance.
Planning as programming is an approach to automated planning, where the planning domain model is expressed as a program in some (declarative) programming language. then the modeler can exploit all features of that lan...
详细信息
Concurrent switching of flip-flops and logic gates produces a current surge in synchronous circuits resulting in power supply noise and integrity issues. It is well known that peak current caused by simultaneous switc...
详细信息
ISBN:
(纸本)9781467387002
Concurrent switching of flip-flops and logic gates produces a current surge in synchronous circuits resulting in power supply noise and integrity issues. It is well known that peak current caused by simultaneous switching can be reduced by clock skew scheduling. It has been shown that this problem may be formulated as an integer linear programming problem. However, such formulation is computationally expensive for designs with large number of flip-flops. In this work, we propose a fast heuristic method to schedule clock skew for reducing peak current. the proposed method is evaluated on ISCAS-89, ITC99 and synthetic benchmark circuits. Results show that the proposed method finds a near-optimal solution within minutes even for the largest benchmark circuits.
In information security, representation and reasoning of authorization policy has been a key research topic in this field especially in a sophisticated information sharing and exchange environment [6, 7, 9]. In such a...
详细信息
ISBN:
(纸本)9781943436040
In information security, representation and reasoning of authorization policy has been a key research topic in this field especially in a sophisticated information sharing and exchange environment [6, 7, 9]. In such a scenario, an user's request to access the system may not be able to decide straightaway, it may initiate a sequence of complex executions of authorization commands in order to determine either to grant or deny such a request. Becker and Nanz's logic of State-Modifying Policies (SMP) is a formal system addressing such problem in access control. In this paper, we provide a declarative semantics for SMP through a translation from SMP to Answer Set programming (ASP) and propose a system prototype to implement our approach. Our experimental results show that our ASP implementation for SMP reasoning is effective to deal with real world problem domains. Copyright ISCA, CAINE 2016.
Model counting is the problem of computing the number of models that satisfy a given propositional theory. It has recently been applied to solving inference tasks in probabilistic logicprogramming, where the goal is ...
详细信息
ISBN:
(纸本)9781577357032
Model counting is the problem of computing the number of models that satisfy a given propositional theory. It has recently been applied to solving inference tasks in probabilistic logicprogramming, where the goal is to compute the probability of given queries being true provided a set of mutually independent random variables, a model (a logic program) and some evidence. the core of solving this inference task involves translating the logic program to a propositional theory and using a model counter. In this paper, we show that for some problems that involve inductive definitions like reachability in a graph, the translation of logic programs to SAT can be expensive for the purpose of solving inference tasks. For such problems, direct implementation of stable model semantics allows for more efficient solving. We present two implementation techniques, based on unfounded set detection, that extend a propositional model counter to a stable model counter. Our experiments show that for particular problems, our approach can outperform a state-of-the-art probabilistic logicprogramming solver by several orders of magnitude in terms of running time and space requirements, and can solve instances of significantly larger sizes on which the current solver runs out of time or memory.
the proceedings of the internationalconference on logicprogramming (ICLP) have had several publishers, including MIT Press and Springer's Lecture Notes in Computer Science. Beginning in 2010, the proceedings hav...
the proceedings of the internationalconference on logicprogramming (ICLP) have had several publishers, including MIT Press and Springer's Lecture Notes in Computer Science. Beginning in 2010, the proceedings have been published in a dual format: with regular papers contained in a special issue of theory and Practice of logicprogramming (TPLP), and technical communications as a Dagstuhl LIPics series publication. the reason for the change was that compared to researchers in other fields, computer scientists publish more in conferences or symposia and less in journals. the thinking went that since many ICLP papers are of journal quality – or nearly so – why not publish them in a journal straight away? And why not TPLP?
Fuzz testing builds confidence in compilers and interpreters. It is desirable for fuzzers to allow targeted generation of programs that showcase specific language features and behaviors. However, the predominant progr...
详细信息
暂无评论