| Description |
1 online resource (xi, 342 pages) : illustrations |
| Series |
Lecture notes in artificial intelligence, 0302-9743 ; 9323 |
|
LNCS sublibrary. SL 7, Artificial intelligence |
|
Lecture notes in computer science. Lecture notes in artificial intelligence ; 9323
|
|
LNCS sublibrary. SL 7, Artificial intelligence.
|
| Contents |
Intro; Preface; Organization; Abstracts of Invited Talks; Contents; Tableaux Calculi; Invited Talk: Coherentisation of First-Order Logic; 1 Definitions; 2 Results; 3 Significance; A Propositional Tableaux Based Proof Calculus for Reasoning with Default Rules; 1 Introduction; 2 Preliminaries; 2.1 Propositional Tableaux; 2.2 Reasoning with Default Rules; 3 Default Tableaux; 4 Discussion; 5 Conclusions and Further Work; A Tableau for Bundled Strategies; 1 Introduction; 2 Bundles and BATL*; 3 Examples; 4 A Tableau for BATL*; 4.1 Pruning the Tableau; 5 Completeness |
|
Modal Tableau Systems with Blockingand Congruence Closure1 Introduction; 2 Modal Logic K(tr, dp) and a Tableau System for It; 3 Modal Tableau System with Congruence Closure; 4 Semantics and Soundness; 5 Completeness; 6 Ancestor Blocking and Other Forms of Blocking; 7 Conclusion; Generalized Qualitative Spatio-Temporal Reasoning: Complexity and Tableau Method; 1 Introduction; 2 Preliminaries; 3 The L1 Spatiotemporal Logic; 4 Revisiting the Satisfiability Problem in L1; 5 Semantic Tableau for L1; 5.1 Rules for Constructing a Semantic Tableau; 5.2 Systematic Construction of a Semantic Tableau |
|
5.3 Soundness and Completeness of Our Semantic Tableau Method6 Conclusion; Efficient Algorithms for Bounded Rigid E-Unification; 1 Introduction; 1.1 Background and Motivating Example; 2 Preliminaries; 2.1 Congruence Closure; 2.2 The Bounded Rigid E-Unification Problem; 3 Solving Bounded Rigid E-Unification; 3.1 Candidate Representation; 4 Eager Encoding of Bounded Rigid E-Unification; 4.1 Congruence Tables; 4.2 Modeling Congruence Tables Using SAT; Eager Procedure; 5 Complemented Congruence Closure; 5.1 Properties of Complemented Congruence Closure |
|
6 Lazily Solving Bounded Rigid E-Unification7 Experiments; 7.1 Results and Discussion; 8 Conclusion; Integrating Simplex with Tableaux; 1 Introduction; 2 The Zenon Automated Theorem Prover; 3 The Simplex and the Branch and Bound Methods; 4 Arithmetic Proof Search Rules; 4.1 Rules; 4.2 Soundness; 4.3 Completeness; 5 Arithmetic Instantiation Mechanism; 5.1 Arithmetic Constraint Trees; 5.2 Interleaving with Zenon; 5.3 Limitations of the Simplex Method; 6 Experimental Results and Proof Certification; 7 Related Work; 8 Conclusion; Efficient Low-Level Connection Tableaux; 1 Introduction |
|
2 leanCoP and Restricted Backtracking3 Low-Level Implementation; 4 Evaluation; 5 Conclusion; Sequent Calculus; A Sequent Calculus for Preferential Conditional Logic Based on Neighbourhood Semantics; 1 Introduction; 2 The Logic PCL; 3 A Labelled Sequent Calculus; 4 Completeness and Termination; 5 Conclusions; Linear Nested Sequents, 2-Sequents and Hypersequents; 1 Introduction; 2 Preliminaries: Nested Sequents and 2-Sequents; 2.1 Nested Sequents / Tree-Hypersequents; 2-Sequents; 3 Linear Nested Sequents for KD; 4 Connections to Sequent Calculi; 4.1 Other Modal Logics; Intuitionistic Logic |
| Summary |
This book constitutes the refereed proceedings of the 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2015, held in Wroclaw, Poland, in September 2015. The 19 full papers and 2 papers presented in this volume were carefully reviewed and selected from 34 submissions. They are organized in topical sections named: tableaux calculi; sequent calculus; resolution; other calculi; and applications |
| Notes |
International conference proceedings |
|
Includes author index |
|
Online resource; title from PDF title page (SpringerLink, viewed September 17, 2015) |
| Subject |
Automatic theorem proving -- Congresses
|
|
Automatic theorem proving
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Nivelle, Hans, editor
|
| ISBN |
9783319243122 |
|
3319243128 |
|
