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.
Codatatypes are absent from many programming and specification languages. We make a case for their importance by revisiting a classical result: the completeness theorem for first-order logic established through a Gent...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
Codatatypes are absent from many programming and specification languages. We make a case for their importance by revisiting a classical result: the completeness theorem for first-order logic established through a Gentzen system. the core of the proof establishes an abstract property of possibly infinite derivation trees, independently of the concrete syntax or inference rules. this separation of concerns simplifies the presentation. the abstract proof can be instantiated for a wide range of Gentzen and tableau systems as well as various flavors of first-order logic. the corresponding Isabelle/HOL formalization demonstrates the recently introduced support for codatatypes and the Haskell code generator.
Proving termination automatically for programs with explicit pointer arithmetic is still an open problem. To close this gap, we introduce a novel abstract domain that can track allocated memory in detail. We use it to...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
Proving termination automatically for programs with explicit pointer arithmetic is still an open problem. To close this gap, we introduce a novel abstract domain that can track allocated memory in detail. We use it to automatically construct a symbolic execution graph that represents all possible runs of the program and that can be used to prove memory safety. this graph is then transformed into an integer transition system, whose termination can be proved by standard techniques. We implemented this approach in the automated termination prover AProVE and demonstrate its capability of analyzing C programs with pointer arithmetic that existing tools cannot handle.
We describe a method for abbreviating an analytic classical first-order logic by the introduction of a lemma. Our is based on first computing a compressed representation of present in the analytic proof and then a cut...
详细信息
ISBN:
(纸本)9783642287176
We describe a method for abbreviating an analytic classical first-order logic by the introduction of a lemma. Our is based on first computing a compressed representation of present in the analytic proof and then a cut-formula that
the paper provides a new approach for automatedreasoning in a logic Program using extended Petri net models. the design includes extension of classical linear resolution of first order logic clauses by multi-resoluti...
详细信息
ISBN:
(纸本)0769530508
the paper provides a new approach for automatedreasoning in a logic Program using extended Petri net models. the design includes extension of classical linear resolution of first order logic clauses by multi-resolution, where a set of clauses can be resolved concurrently without sacrificing any inference, thereby speeding-up the execution of the logic program. the speed-tip and utilization rate of resources are used as the performance evaluation metric to compare the performance of the proposed system withthe classical one.
LPEQ and DLPEQ, two translators for automated equivalence testing of logic programs are discussed. the translators LPEQ and DLPEQ have been implemented in the C programming language under the Linux operating system. B...
详细信息
ISBN:
(纸本)354020721X
LPEQ and DLPEQ, two translators for automated equivalence testing of logic programs are discussed. the translators LPEQ and DLPEQ have been implemented in the C programming language under the Linux operating system. Both translators take two logic programs and command line options as their input and produce a translation for equivalence testing as their output. the input files are assumed to be in an internal format, as produced by the front-end lparSE of the SMODELS system.
Many NP-complete problems can be encoded in the answer set semantics of logic programs in a very concise way, where the encoding reflects the typical "guess and check" nature of NP problems: the property is ...
详细信息
ISBN:
(纸本)354020721X
Many NP-complete problems can be encoded in the answer set semantics of logic programs in a very concise way, where the encoding reflects the typical "guess and check" nature of NP problems: the property is encoded in a way such that polynomial size certificates for it correspond to stable models of a program. However, the problem-solving capacity of full disjunctive logic programs (DLPs) is beyond NP at the second level of the polynomial hierarchy. While problems there also have a "guess and check" structure, an encoding in a DLP is often non-obvious, in particular if the "check" itself is co-NP-complete;usually, such problems are solved by interleaving separate "guess" and "check" programs, where the check is expressed by inconsistency of the check program. We present general transformations of head-cycle free (extended) logic programs into stratified disjunctive logic programs which enable one to integrate such "guess" and "check" programs automatically into a single disjunctive logic program. Our results complement recent results on meta-interpretation in ASP, and extend methods and techniques for a declarative "guess and check" problem solving paradigm through ASP.
the proceedings contain 30 papers. the special focus in this conference is on Nonmononic reasoning and Descriptive complexity. the topics include: On the complexity of theory curbing;graph operations and monadic secon...
ISBN:
(纸本)3540412859
the proceedings contain 30 papers. the special focus in this conference is on Nonmononic reasoning and Descriptive complexity. the topics include: On the complexity of theory curbing;graph operations and monadic second-order logic;efficient first order functional program interpreter with time bound certifications;encoding temporal logics in executable Z;behavioural constructor implementation for regular algebras;an extensible proof text editor;a tactic language for the system Coq;proof simplification for model generation and its applications;compiling and verifying security protocols;equational binary decision diagrams;a PVS proof obligation generator for lustre programs;efficient structural information analysis for real CLP languages;playing logic programs withthe alpha-beta algorithm;logicprogramming approaches for representing and solving constraint satisfaction problems;proof-search in implicative linear logic as a matching problem;a new model construction for the polymorphic lambda calculus;church’s lambda delta calculus;querying inconsistent databases;static reduction analysis for imperative object oriented languages;an abstract interpretation approach to termination of logic programs and using an abstract representation to specialize functional logic programs.
在线阅读本书 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
We handle finite graphs in two ways, as relational structures on the one hand, and as algebraic objects, i.e., as elements of algebras, based on graph operations on the other.
ISBN:
(纸本)3540412859
We handle finite graphs in two ways, as relational structures on the one hand, and as algebraic objects, i.e., as elements of algebras, based on graph operations on the other.
暂无评论