this book constitutes the proceedings of the 18thinternationalconference on logic for programming, Artificial Intelligence, and reasoning, lpar-18, held in Merida, Venezuela, in March 2012. the 25 regular papers and...
详细信息
ISBN:
(数字)9783642287176
ISBN:
(纸本)9783642287169
this book constitutes the proceedings of the 18thinternationalconference on logic for programming, Artificial Intelligence, and reasoning, lpar-18, held in Merida, Venezuela, in March 2012. the 25 regular papers and 6 tool descriptions and experimental papers presented were carefully reviewed and selected from 74 submissions.
the series of internationalconferences on logic for programming, Artificial Intelligence and reasoning (lpar) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automatedreasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world.
Datalog is a well-known database query language based on the logicprogramming paradigm. A general datalog program consists of a number of rules and facts. Programs containing a unique rule and possibly some facts are...
详细信息
ISBN:
(纸本)3540664920
Datalog is a well-known database query language based on the logicprogramming paradigm. A general datalog program consists of a number of rules and facts. Programs containing a unique rule and possibly some facts are called single rule programs (sirups). We study boththe combined and the program complexity of sirups, ie., the complexity of evaluating sirups over variable and fixed databases, respectively. Moreover, we study the descriptive complexity of sirups, i.e., their expressive power. In ail cases it turns out that even very restricted classes of sirups have the same complexity and essentially the same expressive power as general datalog programs. We show that the evaluation of single clause programs is EXPTIME complete (combined complexity), and, if restricted to linear recursive rules, PSPACE complete. Moreover, sirups with one recursive rule and one additional fact capture PTIME on ordered structures, if a certain data representation is assumed and certain predefined relations are provided. Our results are obtained by a uniform product construction which maps a datalog program into a single rule by essentially maintaining its semantics. We also prove that the datalog clause implication problem, i.e., deciding whether a datalog clause implies another one, is EXPTIME complete.
CHAT offers an Eilternative to SLG-WAM for implementing the suspension eind resumption of consumers that tabling needs;unlike SLG-WAM, it does not use freeze registers nor a complicated trail to preserve their executi...
详细信息
ISBN:
(纸本)3540664920
CHAT offers an Eilternative to SLG-WAM for implementing the suspension eind resumption of consumers that tabling needs;unlike SLG-WAM, it does not use freeze registers nor a complicated trail to preserve their execution environments. CHAT Eilso limits the amount of copying of CAT, which was previously put forwMd as another alternative to SLG-WAM. Although experimented results show that in preictice CHAT is competitive with - if not better than - SLG-WAM, there remains the annoying fact that on contrived programs the original CHAT can be made axbitraxily worse than SLG-WAM, i.e. the origincd CHAT has an intrinsically higher complexity. In this paper we show how to overcome this problem, in particular, we deal withthe two sources of higher complexity of CHAT: the repeated traversal of the choice point stack, Eind the lack of sufficient sharing of the trail. this is eichieved without fundamentally changing the underlying principle of CHAT by a technique that manipulates a Prolog choice point so that it assumes temporarily a different functionality smd in a way that is treinsparent to the underlying WAM. there is more potential use of this technique besides lowering the worst case complexity of CHAT: it leads to considering scheduling strategies that were not feasible before either in CHAT or in SLG-WAM. We aJso discuss extensively issues related to the implementation of the trail in a tabled logicprogramming system.
In this paper we continue to develop the approach to automated search for theorem proofe started in Kyiv in 1960-1970s. this approatch presupposes the development of deductive techniques used for the processing of mat...
详细信息
ISBN:
(纸本)3540664920
In this paper we continue to develop the approach to automated search for theorem proofe started in Kyiv in 1960-1970s. this approatch presupposes the development of deductive techniques used for the processing of mathematical texts, written in a formal first-order language, close to the natural language used in mathematical papers. We construct two logical caJculi, gS tnd mS, satisfying the following requirements: the syntacticetl form of the initial problem should be preserved;the proof search should be goal-oriented;preliminary skolemization is not obligatory;equality handling should be sepeurated from the deduction process. the calculus gS is a machine-oriented sequent-type csilculus with "large-block" inference rules for first-order classical logic. the calculus mS is a further development of the calculus gS, enriched with formal analogs of the natursil proof sesurch techniques such as definition handling and application of auxiliary propositions. the results on soundness and completeness of gS and mS aie given.
this volume contains the papers presented at the Sixthinternationalconference on logic for programming and automatedreasoning (lpar'99), held in Tbilisi, Georgia, September 6-10, 1999, and hosted by the Univers...
详细信息
ISBN:
(数字)9783540482420
ISBN:
(纸本)9783540664925
this volume contains the papers presented at the Sixthinternationalconference on logic for programming and automatedreasoning (lpar'99), held in Tbilisi, Georgia, September 6-10, 1999, and hosted by the University of Tbilisi. Forty-four papers were submitted to lpar'99. Each of the submissions was reviewed by three program committee members and an electronic program com mittee meeting was held via the Internet. Twenty-three papers were accepted. We would like to thank the many people who have made lpar'99 possible. We are grateful to the following groups and individuals: to the program committee and the additional referees for reviewing the papers in a very short time, to the organizing committee, and to the local organizers of the INTAS workshop in Tbilisi in April 1994 (Khimuri Rukhaia, Konstantin Pkhakadze, and Gela Chankvetadze). And last but not least, we would like to thank Konstantin - rovin, who maintained the program committee Web page; Uwe Waldmann, who supplied macros for these proceedings and helped us to install some programs for the electronic management of the program committee work; and Bill McCune, who implemented these programs.
the proceedings contain 12 papers. the topics discussed include: properties of answer set programming with convex generalized atoms;hybrid automatedreasoning tools: from black-box to clear-box integration;aspartame: ...
the proceedings contain 12 papers. the topics discussed include: properties of answer set programming with convex generalized atoms;hybrid automatedreasoning tools: from black-box to clear-box integration;aspartame: solving constraint satisfaction problems with answer set programming;a functional view of strong negation in answer set programming;an algebra of causal chains;query answering in object oriented knowledge bases in logicprogramming: description and challenge for ASP;the DIAMOND system for argumentation: preliminary report;a system for interactive query answering with answer set programming;and generating shortest synchronizing sequences using answer set programming.
In this work, the notion of provability for first order linear temporal logic over finite time structures, FO-LTLfin, is studied. We show that the validity problem for such a logic is not recursively enumerable, hence...
详细信息
ISBN:
(纸本)3540664920
In this work, the notion of provability for first order linear temporal logic over finite time structures, FO-LTLfin, is studied. We show that the validity problem for such a logic is not recursively enumerable, hence FO-LTLfin is not recursively axiomatizable. this negative result however does not hold in the case of bounded validity, that is truth in all temporal models where the object domain is possibly infinite, but the underlying sequence of time points does not exceed a given size. A formula is defined to be A-valid if it is true in all tempered models whose underlying time frtime is not greater them κ, where κ is any fixed positive integer. In this work a tableau calculus is defined, that is sound and complete with respect to κ-validity, when given as input the initial formula and the bound κ on the size of the temporal models. the main feature of the system, extending the prepositional calculus defined in [7], is that of explicitly denoting time points and having tableau nodes labelled by either expressions intuitively stating that a formula holds in a given temporal interval or "temporal constraints" i.e. linear inequalities on time points. Branch closure is reduced to unsatisfiability over the integers of the set of temporal constraints in the branch.
Recently, researchers in answer set programming and constraint programming spent significant efforts in the development of hybrid languages and solving algorithms combining the strengths of these traditionally separat...
详细信息
the proceedings contain 30 papers. the special focus in this conference is on Artificial Intelligence, automatedreasoning, and Symbolic Computation. the topics include: Expressiveness and complexity of full first-ord...
ISBN:
(纸本)3540438653
the proceedings contain 30 papers. the special focus in this conference is on Artificial Intelligence, automatedreasoning, and Symbolic Computation. the topics include: Expressiveness and complexity of full first-order constraints in the algebra of trees;deduction versus computation;integration of quantifier elimination with constraint logicprogramming;towards a hybrid symbolic/numeric computational approach in controller design;inductive synthesis of functional programs;on a generalised logicality theorem;using symbolic computation in an automated sequent derivation system for multi-valued logic;multicontext logic for semigroups of contexts;indefinite integration as a testbed for developments in multi-agent systems;genetic symbolic classification integrated with non-linear coefficient optimisation;a novel face recognition method;non-commutative logic for hand-written character modeling;from numerical to symbolic data during the recognition of scenarii;on mathematical modeling of networks and implementation aspects;continuous first-order constraint satisfaction;reasoning and scheduling with interval constraints;a genetic-based approach for satisfiability problems;the meaning of infinity in calculus and computer algebra systems and making conjectures about maple functions.
E-unification (i.e. solving equations modulo an equational theory E) is an essential technique in automatedreasoning, functional logicprogramming and symbolic constraint solving but, in general E-unification is unde...
详细信息
暂无评论