Automated Reasoning Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004. Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Basin, David (Επιμελητής έκδοσης), Rusinowitch, Michaël (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2004.
• Σειρά: Lecture Notes in Computer Science, 3097
• Θέματα: Computer science.; Software engineering.; Computer logic.; Mathematical logic.; Artificial intelligence.; Computer Science.; Artificial Intelligence (incl. Robotics).; Mathematical Logic and Foundations.; Mathematical Logic and Formal Languages.; Logics and Meanings of Programs.; Software Engineering.

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...

Πίνακας περιεχομένων:

• 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.