Intuitionistic Public Announcement logic (IntPAL) proposed by Ma et al. (2014) aims at formalizing changes of an agent's knowledge in a constructive manner. IntPAL can be regarded as an intuitionistic generalizati...
详细信息
ISBN:
(数字)9783662488997
ISBN:
(纸本)9783662488997;9783662488980
Intuitionistic Public Announcement logic (IntPAL) proposed by Ma et al. (2014) aims at formalizing changes of an agent's knowledge in a constructive manner. IntPAL can be regarded as an intuitionistic generalization of Public Announcement logic (PAL) whose modal basis is the intuitionistic modal logic IK by Fischer Servi (1984) and Simpson (1994). We also refer to IK for the basis of this paper. Meanwhile, Nomura et al. (2015) provided a cut-free labelled sequent calculus based on the study of Maffezioli et al. (2010). In this paper, we introduce a labelled sequent calculus for IntPAL (we call it GIntPAL) as both an intuitionistic variant of GPAL and a public announcement extension of Simpson's labelled calculus, and show that all theorems of the Hilbert axiomatization of IntPAL are also derivable in GIntPAL withthe cut rule. then we prove the admissibility of the cut rule in GIntPAL and also the soundness result for birelational Kripke semantics. Finally, we derive the semantic completeness of GIntPAL as a corollary of these theorems.
Advances in the Internet of things and the Web of Data created huge opportunities for developing applications that can generate actionable knowledge out of streaming data. the trade-off between scalability and express...
详细信息
ISBN:
(数字)9783319220024
ISBN:
(纸本)9783319220024;9783319220017
Advances in the Internet of things and the Web of Data created huge opportunities for developing applications that can generate actionable knowledge out of streaming data. the trade-off between scalability and expressivity is a key challenge in this setting, and more investigation is required to identify what are the relevant features in optimizing this trade-off, and what role do they have in the optimization. In this paper we motivate the need for heuristics to design adaptive solutions and, following an empirical approach, we highlight some key concepts and ideas that can guide the design of heuristics for adaptive optimization of Web Stream reasoning.
Heuristic search is arguably the most successful paradigm in automated Planning, which greatly improves the performance of planning strategies. However, adding heuristics usually leads to very complicated planning alg...
详细信息
ISBN:
(数字)9783319220024
ISBN:
(纸本)9783319220024;9783319220017
Heuristic search is arguably the most successful paradigm in automated Planning, which greatly improves the performance of planning strategies. However, adding heuristics usually leads to very complicated planning algorithms. In order to study different properties (e.g. completeness) of those complicated planning algorithms, it is important to use an appropriate formal language and framework. In this paper, we argue that Transaction logic is just such a specification language, which lets one formally specify boththe heuristics, the planning algorithm, and also facilitates the discovery of more general and more efficient algorithms. To illustrate, we take the well-known regression analysis mechanism and show that Transaction logic lets one specify the concept of regression analysis easily and thus express RSTRIPS, a classical and very complicated planning algorithm based on regression analysis. Moreover, we show that extensions to that algorithm that allow indirect effects and action ramification are obtained almost for free. Finally, a compact and clear logical formulation of the algorithm lets us prove the completeness of RSTRIPS-aresult that, to the best of our knowledge, has not been known before.
In the travel industry it is common for tour operators to pre-book from service suppliers blocks of package tours, which are called allotments in jargon. the selection of package tours is done according to several pre...
详细信息
ISBN:
(数字)9783319220024
ISBN:
(纸本)9783319220024;9783319220017
In the travel industry it is common for tour operators to pre-book from service suppliers blocks of package tours, which are called allotments in jargon. the selection of package tours is done according to several preference criteria aimed at maximizing the expected earnings given a budget. In this paper we formalize an allotment problem that abstracts the requirements of a real travel agent, and we solve it using Answer Set programming. the obtained specification is executable, and it implements an advanced feature of the iTravel+ system.
Resource-constrained scheduling problems appear frequently at different levels of decisions in manufacturing, logistics, computer networks, software engineering etc. they are usually characterized by many types of con...
详细信息
ISBN:
(纸本)9783319248349;9783319248332
Resource-constrained scheduling problems appear frequently at different levels of decisions in manufacturing, logistics, computer networks, software engineering etc. they are usually characterized by many types of constraints, which often make them unstructured and difficult to solve (NP-complete). Traditional mathematical programming (MP) approaches are deficient because their representation of allocation constraints is artificial (using 0-1 variables). Unlike traditional approaches, declarative constraint logicprogramming (CLP) provides for a natural representation of heterogeneous constraints. In CLP we state the problem requirements by constraints;we do not need to specify how to meet these requirements. CLP approach is very effective for binary constraints (binding at most two variables). If there are more variables in the constraints and the problem requires further optimization, the efficiency decreases dramatically. this paper presents a hybrid programming framework for constrained scheduling problems where two environments (mathematical programming and constraint logicprogramming) were integrated. this integration, hybridization as well as a transformation of the problem helped reduce the combinatorial problem substantially. In order to compare the effectiveness of the proposed framework, also made implementation of illustrative example separately for the two environments MP and CLP.
Our Mathematical programming Modulo theories (MPMT) constraint solving framework extends Mathematical programming technology with techniques from the field of automatedreasoning, e.g., solvers for first-order theorie...
详细信息
ISBN:
(纸本)9783319216683;9783319216676
Our Mathematical programming Modulo theories (MPMT) constraint solving framework extends Mathematical programming technology with techniques from the field of automatedreasoning, e.g., solvers for first-order theories. In previous work, we used MPMT to synthesize system architectures for Boeing's Dreamliner and we studied the theoretical aspects of MPMT by means of the Branch and Cut Modulo T (BC(T)) transition system. BC(T) can be thought of as a blueprint for MPMT solvers. this paper provides a more practical and algorithmic view of BC(T). We elaborate on the design and features of Inez, our BC(T) constraint solver. Inez is an open-source, freely available superset of the OCaml programming language that uses the SCIP Branch and Cut framework to extend OCaml with MPMT capability. Inez allows users to write programs that arbitrarily interweave general computation with MPMT constraint solving.
automated algorithm selection techniques have been applied successfully to Answer Set programming (ASP) solvers. ASP computation includes two levels of computation: variable substitution, called grounding, and proposi...
详细信息
Focused proofs are sequent calculus proofs that group inference rules into alternating positive and negative phases. these phases can then be used to define macro-level inference rules Gentzen's original and tiny ...
详细信息
ISBN:
(数字)9783662488997
ISBN:
(纸本)9783662488997;9783662488980
Focused proofs are sequent calculus proofs that group inference rules into alternating positive and negative phases. these phases can then be used to define macro-level inference rules Gentzen's original and tiny introduction and structural rules. We show here that the inference rules of labeled proof systems for modal logics can similarly be described as pairs of such phases within the LKF focused proof system for first-order classical logic. We consider the system G3K of Negri for the modal logic K and define a translation from labeled modal formulas into first-order polarized formulas and show a strict correspondence between derivations in the two systems, i.e., each rule application in G3K corresponds to a bipole-a pair of a positive and a negative phases-in LKF. Since geometric axioms (when properly polarized) induce bipoles, this strong correspondence holds for all modal logics whose Kripke frames are characterized by geometric properties. We extend these results to present a focused labeled proof system for this same class of modal logics and show its soundness and completeness. the resulting proof system allows one to define a rich set of normal forms of modal logic proofs.
In (Guller, 2014), we have generalised the well-known hyperresolution principle to the first-order Gödel logic with truth constants. this paper is a continuation of our work. We propose a hyperresolution calculus...
详细信息
A logic program under the answer set semantics can be inconsistent because its only answer set is the set of all literals, or because it does not have any answer sets. In both cases, the reason for the inconsistency m...
详细信息
暂无评论