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.
this paper presents a general approach to the Abstract Interpretation of Prolog programs with cut. In most of previous approaches the cut primitive is merely ignored. Our method consists in trasforming an interpreter ...
详细信息
A notation for expressing the control algorithms (subgoaling strategies) of natural deduction theorem provers is presented. the language provides tools for building widely known, fundamental theorem proving strategies...
详细信息
在线阅读本书 Book Description this book constitutes the refereed proceedings of the 8thinternationalconference on logic for programming, Artificial Intelligence, and reasoning, lpar 2001, held in Havana, Cuba, in De...
详细信息
ISBN:
(纸本)9783540429579
在线阅读本书 Book Description this book constitutes the refereed proceedings of the 8thinternationalconference on logic for programming, Artificial Intelligence, and reasoning, lpar 2001, held in Havana, Cuba, in December *** 40 revised full papers presented together with an invited paper were carefully reviewed and selected from 112 submissions. the book offers topical sections on verification, guarded logic, agents, automatedtheorem proving, non-classical logics, types, experimental aspects, foundations of logic, CSP and SAT, nonmonotonic reasoning, semantics, termination, knowledge-based systems, analysis of logic programs, databases and knowledge bases, and program analysis and proof planning. Book Dimension length: (cm)23.3 width:(cm)15.4
the proceedings contain 50 papers. the special focus in this conference is on Knowledge Engineering, Case Based reasoning, Planning, Scheduling and Multi-agent Systems. the topics include: Decision-rule solutions for ...
ISBN:
(纸本)354041276X
the proceedings contain 50 papers. the special focus in this conference is on Knowledge Engineering, Case Based reasoning, Planning, Scheduling and Multi-agent Systems. the topics include: Decision-rule solutions for data mining with missing values;getting computer systems to function as team players;case-based management of software engineering experience ware;handling cases and the coverage in a limited quantity of memory for case-based planning systems;integrating rules and cases in learning via case explanation and paradigm shift;the java embedded object production system;global and local search for scheduling job shop with parallel machines;knowledge-based interactive scheduling of multiproduct batch plants;using and evaluating adaptive agents for electronic commerce negotiation;dependence based coalitions and contract net;scheduling meetings through multi-agent negotiation;agents working on the integration of heterogeneous information sources in distributed healthcare environments;solving conflicting beliefs with a distributed belief revision approach;an organizational model for multi-agent systems;evolving populations of agents with personalities in the minority game;using meta-cognitive conflicts to provoke strategic changes;sharing resource-sensitive knowledge using combinator logics;compiling default theory into extended logicprogramming;representing belief revision through default theories;representing operational knowledge by contextual graphs;a new distributed reinforcement learning algorithm for multiple objective optimization problems and cognitive multi-agent systems for integrated information retrieval and extraction over the web.
the proceedings contain 39 papers. the special focus in this conference is on Artificial Intelligence. the topics include: Towards a probabilistic analysis for conditionals and unconditionals;an inference problem set ...
ISBN:
(纸本)9783319509525
the proceedings contain 39 papers. the special focus in this conference is on Artificial Intelligence. the topics include: Towards a probabilistic analysis for conditionals and unconditionals;an inference problem set for evaluating semantic theories and semantic processing systems for Japanese;applicative abstract categorial grammars in full swing;scope parallelism in coordination in dependent type semantics;discourse particles as CCP-modifiers: German doch and ja as context filters;tracking down disjunction;the meaning and use of the Japanese counter-expectational adverbs;evaluative predicates and evaluative uses of ordinary predicates;strong permission in prescriptive causal models;truth as a logical connective;abductive logicprogramming for normative reasoning and ontologies;a belief revision technique to model civil code updates;using ontologies to model data protection requirements in workflows;utilization of multi-word expressions to improve statistical machine translation of statutory sentences;argumentation support tool with reliability-based argumentation framework;applying a convolutional neural network to legal question answering;lexical-morphological modeling for legal text analysis;on the issue of argumentation and informedness;on the interpretation of assurance case arguments;learning argument acceptability from abstract argumentation frameworks;designing intelligent sleep analysis systems for automated contextual exploration on personal sleep-tracking data;a comparative study of similarity measures for time series classification;extracting propagation patterns from bacterial culture data in medical facility;aggregating and analyzing articles and comments on a news website;feasibility of collaborative learning and work between robots and children with autism spectrum disorders.
暂无评论