Automated Reasoning
Subtitle: First International Joint Conference, IJCAR 2001 Siena, Italy, June 18-23, 2001 Proceedings (Lecture Notes in Computer Science)
Contributors: Rajeev Gore (Editor); Alexander Leitsch (Editor); Tobias Nipkow (Editor)
Edition: 1 edition
Publisher: Springer
Published: August 9, 2001
Language: eng
Format: Paperback
Number of pages: 708
ISBN-13: 9783540422549
Subjects: Artificial intelligence; Expert Systems; Computer Logic; Automata; Computers; Computers - General Information; Congresses; Computer Books: General; Computer Science; Artificial Intelligence - General; General; AI logics; Automated reasoning; Computers / Artificial Intelligence; autmated deduction; first-order-logic; formal logic; inference; Automatic theorem proving
First sentence: Size-change analysis is based on size-change graphs giving local approximations to parameter size changes derivable from program syntax.
Description: Automated Reasoning: First International Joint Conference, IJCAR 2001 Siena, Italy, June 18–22, 2001 Proceedings<br />Author: Rajeev Goré, Alexander Leitsch, Tobias Nipkow<br /> Published by Springer Berlin Heidelberg<br /> ISBN: 978-3-540-42254-9<br /> DOI: 10.1007/3-540-45744-5<br /><br />Table of Contents:<p></p><ul><li>Program Termination Analysis by Size-Change Graphs (Abstract)
</li><li>SET Cardholder Registration: The Secrecy Proofs
</li><li>Algorithms, Datastructures, and other Issues in Efficient Automated Deduction
</li><li>The Description Logic ALCNH
</li><li>NExpTime-Complete Description Logics with Concrete Domains
</li><li>Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics
</li><li>The Hybrid μ-Calculus
</li><li>The Inverse Method Implements the Automata Approach for Modal Satisfiability
</li><li>Deduction-Based Decision Procedure for a Clausal Miniscoped Fragment of FTL
</li><li>Tableaux for Temporal Description Logic with Constant Domains
</li><li>Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-rigid Designation
</li><li>Instructing Equational Set-Reasoning with Otter
</li><li>NP-Completeness of Refutability by Literal-Once Resolution
</li><li>Ordered Resolution vs. Connection Graph resolution
</li><li>A Model-Based Completeness Proof of Extended Narrowing and Resolution
</li><li>A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality
</li><li>Superposition and Chaining for Totally Ordered Divisible Abelian Groups
</li><li>Context Trees
</li><li>On the Evaluation of Indexing Techniques for Theorem Proving
</li><li>Preferred Extensions of Argumentation Frameworks: Query, Answering, and Computation</li></ul>