Automated Reasoning : Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings / edited by David Basin, Michael Rusinowitch.

Format:

Book

Contributor:

Basin, David, editor.

Rusinowitch, M. (Michael), editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

Lecture notes in computer science. Lecture notes in artificial intelligence ; 3097.

Lecture Notes in Artificial Intelligence ; 3097

Language:

English

Subjects (All):

Artificial intelligence.

Logic, Symbolic and mathematical.

Computer logic.

Software engineering.

Artificial Intelligence.

Mathematical Logic and Foundations.

Mathematical Logic and Formal Languages.

Logics and Meanings of Programs.

Software Engineering.

Local Subjects:

Artificial Intelligence.

Mathematical Logic and Foundations.

Mathematical Logic and Formal Languages.

Logics and Meanings of Programs.

Software Engineering.

Physical Description:

1 online resource (XII, 491 pages).

Edition:

First edition 2004.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2004.

System Details:

text file PDF

Summary:

This volume constitutes the proceedings of the 2nd International Joint C- ference on Automated Reasoning (IJCAR 2004) held July 4-8, 2004 in Cork, Ireland. IJCAR 2004 continued the tradition established at the ?rst IJCAR in Siena,Italyin2001,whichbroughttogetherdi?erentresearchcommunitieswo- ing in automated reasoning. The current IJCAR is the fusion of the following conferences: CADE: The International Conference on Automated Deduction, CALCULEMUS: Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, FroCoS: Workshop on Frontiers of Combining Systems, FTP: The International Workshop on First-Order Theorem Proving, and TABLEAUX: The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. There were 74 research papers submitted to IJCAR as well as 12 system descriptions. After extensive reviewing, 26 research papers and 6 system - scriptions were accepted for presentation at the conference and publication in this volume. In addition, this volume also contains papers from the three invited speakers and a description of the CADE ATP system competition. We would like to acknowledge the enormous amount of work put in by the members of the program committee, the various organizing and steering c- mittees, the IJCAR o?cials, the invited speakers, and the additional referees named on the following pages. We would also like to thank Achim Brucker and Barbara Geiser for their help in producing this volume.

Contents:

Rewriting

Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools

A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting

Efficient Checking of Term Ordering Constraints

Improved Modular Termination Proofs Using Dependency Pairs

Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure

Saturation-Based Theorem Proving

Redundancy Notions for Paramodulation with Non-monotonic Orderings

A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards

Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures

Combination Techniques

Decision Procedures for Recursive Data Structures with Integer Constraints

Modular Proof Systems for Partial Functions with Weak Equality

A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics

Verification and Systems

Using Automated Theorem Provers to Certify Auto-generated Aerospace Software

argo-lib: A Generic Platform for Decision Procedures

The ICS Decision Procedures for Embedded Deduction

System Description: E 0.81

Reasoning with Finite Structure

Second-Order Logic over Finite Structures - Report on a Research Programme

Efficient Algorithms for Constraint Description Problems over Finite Totally Ordered Domains

Tableaux and Non-classical Logics

PDL with Negation of Atomic Programs

Counter-Model Search in Gödel-Dummett Logics

Generalised Handling of Variables in Disconnection Tableaux

Applications and Systems

Chain Resolution for the Semantic Web

Sonic - Non-standard Inferences Go OilEd

TeMP: A Temporal Monodic Prover

Dr.Doodle: A Diagrammatic Theorem Prover

Computer Mathematics

Solving Constraints by Elimination Methods

Analyzing Selected Quantified Integer Programs

Interactive Theorem Proving

Formalizing O Notation in Isabelle/HOL

Experiments on Supporting Interactive Proof Using Resolution

A Machine-Checked Formalization of the Generic Model and the Random Oracle Model

Combinatorial Reasoning

Automatic Generation of Classification Theorems for Finite Algebras

Efficient Algorithms for Computing Modulo Permutation Theories

Overlapping Leaf Permutative Equations

Higher-Order Reasoning

TaMeD: A Tableau Method for Deduction Modulo

Lambda Logic

Formalizing Undefinedness Arising in Calculus

Competition

The CADE ATP System Competition.

Other Format:

Printed edition:

ISBN:

978-3-540-25984-8

9783540259848

Access Restriction:

Restricted for use by site license.