Return to home page
Searching: Otterbein library catalog
Some OPAL libraries remain closed or are operating at reduced service levels. Materials from those libraries may not be requestable; requested items may take longer to arrive. Note that pickup procedures may differ between libraries. Please contact your library for new procedures, specific requests, or other assistance.
  Previous Record Previous Item Next Item Next Record
  Reviews, Summaries, etc...
EBOOK
Conference TABLEAUX (Conference) (24th : 2015 : Wrocław, Poland) (Wrocaw, Poland)
Title Automated reasoning with analytic tableaux and related methods : 24th International Conference, TABLEAUX 2015, Wrocaw, Poland, September 21-24, 2015. Proceedings / Hans De Nivelle (ed.).
Imprint Cham : Springer, 2015.

LOCATION CALL # STATUS MESSAGE
 OHIOLINK SPRINGER EBOOKS    ONLINE  
View online
Conference TABLEAUX (Conference) (24th : 2015 : Wrocław, Poland) (Wrocaw, Poland)
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.
Subject Automatic theorem proving -- Congresses.
Alt Name Nivelle, Hans,
Add Title TABLEAUX 2015
LOCATION CALL # STATUS MESSAGE
 OHIOLINK SPRINGER EBOOKS    ONLINE  
View online
Conference TABLEAUX (Conference) (24th : 2015 : Wrocław, Poland) (Wrocaw, Poland)
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.
Subject Automatic theorem proving -- Congresses.
Alt Name Nivelle, Hans,
Add Title TABLEAUX 2015
Description 1 online resource (xi, 342 pages) : illustrations.
polychrome rdacc
Note International conference proceedings.
Includes author index.
Online resource; title from PDF title page (SpringerLink, viewed September 17, 2015).
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.
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
ISBN 9783319243122 (electronic bk.)
3319243128 (electronic bk.)
9783319243115
ISBN/ISSN 10.1007/978-3-319-24312-2
OCLC # 921302601


If you experience difficulty accessing or navigating this content, please contact the OPAL Support Team