This paper describes a new format for representing Tarskian-style interpretations for formulae in typed first-order logic, using the TPTP TF0 language. It further describes a technique and an implemented tool for veri...
详细信息
logic for programming and automatedreasoning : 6Th internationalconference, lpar'99, Tbilisi, Georgia, September 6-10, 1999 : Proceedings by lpar '99 (1999 : Tʻbilisi, Georgia); Ganzinger, H. (Harald), 1950-...
详细信息
logic for programming and automatedreasoning : 6Th internationalconference, lpar'99, Tbilisi, Georgia, September 6-10, 1999 : Proceedings by lpar '99 (1999 : Tʻbilisi, Georgia); Ganzinger, H. (Harald), 1950-; McAllester, David A; Voronkov, A. (Andreĭ), 1959-; published by Berlin ; New York : Springer
The proceedings contain 43 papers. The special focus in this conference is on logic for programming, Artificial Intelligence, and reasoning. The topics include: Skolemization for substructural logics;reasoning about e...
ISBN:
(纸本)9783662488980
The proceedings contain 43 papers. The special focus in this conference is on logic for programming, Artificial Intelligence, and reasoning. The topics include: Skolemization for substructural logics;reasoning about embedded dependencies using inclusion dependencies;a tool for solving general deductive games;on anti-subsumptive knowledge enforcement;value sensitivity and observable abstract values for information flow control;fairly efficient machine learning connection prover;decidability, introduction rules and automata;analyzing internet routing security using model checking;boolean formulas for the static identification of injection attacks in java;an adequate compositional encoding of bigraph structure in linear logic with subexponentials;controller synthesis for MDPs and frequency LT\GU;automated benchmarking of incremental SAT and QBF solvers;a labelled sequent calculus for intuitionistic public announcement logic;implicit computational complexity of subrecursive definitions and applications to cryptographic proofs;tools for inductive provers;verification of concurrent programs using trace abstraction refinement;synchronized recursive timed automata;focused labeled proof systems for modal logic;on subexponentials, synthetic connectives, and multi-level delimited control;on the expressive power of communication primitives in parameterised systems;fine grained SMT proofs for the theory of fixed-width bit-vectors;abstract domains and solvers for sets reasoning;relational reasoning via probabilistic coupling;a contextual logical framework;enhancing search-based QBF solving by dynamic blocked clause elimination;reasoning about loops using vampire in key;compositional propositional proofs;normalisation by completeness with heyting algebras and using program synthesis for program analysis.
The proceedings contain 34 papers. The topics discussed include: automatic inference of resource consumption bounds;matrix interpretations for polynomial derivational complexity of rewrite systems;parameterized comple...
ISBN:
(纸本)9783642287169
The proceedings contain 34 papers. The topics discussed include: automatic inference of resource consumption bounds;matrix interpretations for polynomial derivational complexity of rewrite systems;parameterized complexity and fixed-parameter tractability of description logicreasoning;enfragmo: a system for modeling and solving search problems with logic;automated and human proofs in general mathematics: an initial comparison;lazy abstraction with interpolants for arrays;backward trace slicing for conditional rewrite theories;forgetting for defeasible logic;solving language equations and disequations with applications to disunification in description logics and monadic set constraints;dual-priced modal transition systems with time durations;finding finite herbrand models;and monitor-based statistical model checking for weighted metric temporal logic.
The fragment of propositional logic known as Horn theories plays a central role in automatedreasoning. The problem of enumerating the maximal models of a Horn theory (MAXMOD) has been proved to be computationally har...
详细信息
The TPTP World is a well established infrastructure supporting research, development, and deployment of automated Theorem Proving systems. Recently, the TPTP World has been extended to include a typed first-order logi...
详细信息
ISBN:
(纸本)9783642287176
The TPTP World is a well established infrastructure supporting research, development, and deployment of automated Theorem Proving systems. Recently, the TPTP World has been extended to include a typed first-order logic, which in turn has enabled the integration of arithmetic. This paper describes these developments.
The proceedings contain 28 papers. The special focus in this conference is on logic for programming. The topics include: logic and computation in a lambda calculus with intersection and union types;graded alternating-...
ISBN:
(纸本)9783642175107
The proceedings contain 28 papers. The special focus in this conference is on logic for programming. The topics include: logic and computation in a lambda calculus with intersection and union types;graded alternating-time temporal logic;non-oblivious strategy improvement;a simple class of kripke-style models in which logic and computation have equal standing;Label-free proof systems for intuitionistic modal logic IS5;an intuitionistic epistemic logic for sequential consistency on shared memory;disunification for ultimately periodic interpretations;synthesis of trigger properties;semiring-induced propositional logic: Definition and basic algorithms;speed-up techniques for negation in grounding;dafny: An automatic program verifier for functional correctness;relentful strategic reasoning in alternating-time temporal logic;counting and enumeration problems with bounded treewidth;the nullness analyser of julia;Qex: Symbolic SQL query explorer;automated proof compression by invention of new definitions;atomic cut introduction by resolution: Proof structuring and compression;satisfiability of Non-linear (Ir)rational arithmetic;coping with selfish on-going behaviors;constraint-Based Abstract Semantics for Temporal logic: A Direct Approach to Design and Implementation;on the equality of probabilistic terms;program logics for homogeneous meta-programming;verifying pointer and string analyses with region type systems;ABC: Algebraic bound computation for loops;hardness of preorder checking for basic formalisms;a quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae.
This book constitutes the refereed proceedings of the 15th internationalconference on logic for programming, Artificial Intelligence, and reasoning, lpar 2008, which took place in Doha, Qatar, during November 22-27, ...
详细信息
ISBN:
(数字)9783540894391
ISBN:
(纸本)9783540894384
This book constitutes the refereed proceedings of the 15th internationalconference on logic for programming, Artificial Intelligence, and reasoning, lpar 2008, which took place in Doha, Qatar, during November 22-27, 2008. The 45 revised full papers presented together with 3 invited talks were carefully revised and selected from 153 submissions. The papers address all current issues in automatedreasoning, computational logic, programming languages and their applications and are organized in topical sections on automata, linear arithmetic, verification knowledge representation, proof theory, quantified constraints, as well as modal and temporal logics.
The proceedings contain 50 papers. The topics discussed include: independently checkable proofs from decision procedures: issues and progress;Zap: automated theorem proving for software analysis;scaling up: computers ...
详细信息
The proceedings contain 50 papers. The topics discussed include: independently checkable proofs from decision procedures: issues and progress;Zap: automated theorem proving for software analysis;scaling up: computers vs. common sense;a new constraint solver for 3D lattices and its application to the protein folding problem;disjunctive constraint lambda calculi;optimizing the runtime processing of types in polymorphic logicprogramming languages;the four sons of penrose;termination of fair computations in term rewriting;matching with regular constraints;automating coherent logic;regular derivations in basic superposition-based calculi;on the specification on sequent systems;experimental evaluation of classical automata constructions;reasoning about incompletely defined programs;a unified memory model for pointers;pushdown module checking;functional correctness proofs of encryption algorithms;and algebraic intruder deductions.
Congruence closure algorithms for deduction in ground equational theories are ubiquitous in many (semi-)decision procedures used for verification and automated deduction. They axe also frequently used in practical con...
详细信息
ISBN:
(数字)9783540398134
ISBN:
(纸本)3540201017
Congruence closure algorithms for deduction in ground equational theories are ubiquitous in many (semi-)decision procedures used for verification and automated deduction. They axe also frequently used in practical contexts where some interpreted function symbols are present. In particular, for the verification of pipelined microprocessors, in many cases it suffices to be able to deal with integer offsets, that is, instead of only having ground terms t built over free symbols, all (sub)terms can be of the form t + k for arbitrary integer values k. In this paper we first give a different very simple and clean formulation for the standard congruence closure algorithm which we believe is of interest on itself. It builds on ideas from the abstract algorithms of [Kap97,BT00], but it is easily shown to run in the best known time, O(n log n), like the classical algorithms [DST80,NO80,Sho84]. After that, we show how this algorithm can be smoothly extended to deal with integer offsets without increasing this asymptotic complexity.
暂无评论