In this paper we propose a non-clausal representational formalism (of definite formulas) that retains the syntactic flavor and algorithmic advantages of Horn clauses. the notion of a definite formula is generic in the...
详细信息
the proceedings contain 40 papers. the topics discussed include: the gain of failures: using side-effects of anaphora resolution for term consistency checks;constraint solving in logicprogramming and in automated ded...
ISBN:
(纸本)354064993X
the proceedings contain 40 papers. the topics discussed include: the gain of failures: using side-effects of anaphora resolution for term consistency checks;constraint solving in logicprogramming and in automated deduction: a comparison;reasoning about generalized intervals;formalizing belief reports - the approach and a case study;extension calculus and query answering in prioritized default logic;study of symmetry in qualitative temporal interval networks;a blackboard architecture for guiding interactive proofs;combining nonmonotonic reasoning and belief revision: a practical approach;using linear temporal logic to model and solve planning problems;tailorable interactive agents for scheduling meetings;planning diagonalization proofs;theories and proofs in fault diagnosis;nonmonotonic reasoning under uncertain evidence;and planning via model checking in deterministic domains: preliminary report.
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...
详细信息
the proceedings contain 18 papers. the special focus in this conference is on programming Languages and Systems. the topics include: Concurrent constraint programming based on functional programming;a bisimulation met...
ISBN:
(纸本)3540643028
the proceedings contain 18 papers. the special focus in this conference is on programming Languages and Systems. the topics include: Concurrent constraint programming based on functional programming;a bisimulation method for cryptographic protocols;a polyvariant binding-time analysis for off-line partial deduction;complexity of concrete type-inference in the presence of exceptions;an efficient new fixpoint algorithm for distributive constraint systems;reasoning about classes in object-oriented languages;language primitives and type discipline for structured communication-based programming;recursive object types in a logic of object-oriented programs;about modes and states for reactive systems;building a bridge between pointer aliases and program dependences;a complete declarative debugger of missing answers;systematic change of data representation and a generic framework for specialization.
We try to formalize the intuitive reasoning which we normally use to get convinced that a query has successful LD-derivations in a program. To this purpose we dene the class of programs and queries without failures wh...
详细信息
We give a proof-theoretic analysis of logic programs transformations, viewed as operations on proof trees in the sense of [3,4,9,10]. We present a logic for reasoning about (equivalence preserving) transformations of ...
详细信息
Many non-classical logics can be axiomatized by means of Hilbert Systems. reasoning in Hilbert Systems, however, is extremely inefficient. Most inference methods therefore use the semantics of a logic in one kind or a...
详细信息
the proceedings contain 38 papers. the special focus in this conference is on Systems and Tool Demonstrations. the topics include: Duration calculus, a logical approach to real-time systems;abstract algebraic logic;sy...
ISBN:
(纸本)3540654623
the proceedings contain 38 papers. the special focus in this conference is on Systems and Tool Demonstrations. the topics include: Duration calculus, a logical approach to real-time systems;abstract algebraic logic;systematising reactive system design;systematic design of call-coverage features;visual abstractions for temporal verification;a linear metalanguage for concurrency;verification of bounded delay asynchronous circuits with timed traces;verification of temporal properties of processes in a setting with data;a logic for real-time systems specification, its algebraic semantics, and equational calculus;effective recognizability and model checking of reactive fiffo automata;combining methods for the livelock analysis of a fault-tolerant system;separating sets by modal formulas;interpolation in modal logic;building models of linear logic;term rewriting in a logic of special relations;abstraction barriers in equational proof;a synergy between model-checking and type inference for the verification of value-passing higher-order processes;a trace-based refinement calculus for shared-variable parallel programs;consistency of partial process specifications;obervational logic;scheduling algebra;an algebraic approach to combining processes in a hardware/software partitioning environment;an algebraic view of program composition;architectural specifications in CASL;pi-congruences as CCS equivalences;algebraic specifications, higher-order types, and set-theoretic models;type analysis for CHIP;categorical programming with abstract data types;condensing lemmas for pure type systems with universes;abstract interpretation of prolog programs;factorizing equivalent variable pairs in ROBDD-based implementation of pos and a single perspective on arrows between institutions.
this research is aimed at giving a bridge between the two research areas, Inductive logicprogramming and Computational Learning. We focus our attention on four fittings (learning methods) invented in the two areas: S...
详细信息
the advantages and difficulties of representing indefinite information have been studied actively as have been the various solutions proposed for it. One of the difficulties is whether to treat the or operator inclusi...
详细信息
ISBN:
(纸本)9781581130614
the advantages and difficulties of representing indefinite information have been studied actively as have been the various solutions proposed for it. One of the difficulties is whether to treat the or operator inclusively or exclusively. In this paper we show how Lassez's strong model semantics [8] can be used to support inclusive interpretation, and later show that it is also strong enough to provide exclusive interpretation. We investigate its properties and show how it differs from others. We believe that Lassez's strong model semantics is the only "reasonably simple" semantics that support both inclusive and exclusive interpretations. Copyright ACM 1998.
暂无评论