7. TABLEAUX 1998: Oisterwijk, The Netherlands

Extended Abstracts of Invited Lectures

• N. G. de Bruijn:
  Philosophical Aspects of Computerized Verification of Mathematics. 1-9
  
• Alan Bundy:
  A Science of Reasoning (Extended Abstract). 10-17
  
• Edmund M. Clarke, Sergey Berezin:
  Model Checking: Historical Perspective and Example (Extended Abstract). 18-24
  

Comparison

• Peter Balsiger, Alain Heuerding:
  Comparison of Theorem Provers for Modal Logics - Introduction and Summary. 25-26
  
• Ian Horrocks, Peter F. Patel-Schneider:
  FaCT and DLP. 27-30
  
• Michel Levy:
  Prover KT4. 31-32
  
• Bernhard Beckert, Rajeev Goré:
  leanK 2.0. 33-34
  
• Peter Balsiger, Alain Heuerding, Stefan Schwendimann:
  Logics Workbench 1.0. 35-37
  
• Jeremy V. Pitt:
  Benchmark Evaluation of Square-KE. 38-39
  

Abstracts of the Tutorials

• G. L. J. M. Janssen:
  Implementation of Propositional Temporal Logics Using BDDs. 40-41
  
• Ján Komara, Paul J. Voda:
  Computer Programming as Mathematics in a Programming Language and Proof System CL. 42-43
  

Contributed Research Papers

• Matteo Baldoni, Laura Giordano, Alberto Martelli:
  A Tableau for Multimodal Logics and Some (Un)Decidability Results. 44-59
  
• Peter Baumgartner:
  Hyper Tableau - The Next Generation. 60-76
  
• Bernhard Beckert, Dov M. Gabbay:
  Fibring Semantic Tableaux. 77-92
  
• Bernhard Beckert, Ulrike Hartmer:
  A Tableau Calculus for Quantifier-Free Set Theoretic Formulae. 93-107
  
• Howard Bowman, Simon J. Thompson:
  A Tableau Method for Interval Temporal Logic with Projection. 108-123
  
• Serenella Cerrito, Marta Cialdea Mayer:
  Bounded Model Search in Linear Temporal Logic and Its Application to Planning. 124-140
  
• Uwe Egly, Hans Tompits:
  On Proof Complexity of Circumscription. 141-155
  
• Christian G. Fermüller, Herbert Langsteiner:
  Tableaux for Finite-Valued Logics with Arbitrary Distribution Modalities. 156-171
  
• Reiner Hähnle, Neil V. Murray, Erik Rosenthal:
  Some Remarks on Completeness, Connection Graph Resolution and Link Deletion. 173-186
  
• Ullrich Hustadt, Renate A. Schmidt:
  Simplification and Backjumping in Modal Tableau. 187-201
  
• Pedro J. Martín, Antonio Gavilanes, Javier Leach:
  Free Variable Tableaux for a Logic with Term Declarations. 202-216
  
• Fabio Massacci:
  Simplification: A General Constraint Propagation Technique for Propositional and Modal Tableaux. 217-231
  
• Christof Monz, Maarten de Rijke:
  A Tableaux Calculus for Ambiguous Quantification. 232-246
  
• Sara Negri, Jan von Plato:
  From Kripke Models to Algebraic Counter-Valuations. 247-261
  
• Stephan Schmitt, Christoph Kreitz:
  Deleting Redundancy in Proof Reconstruction. 262-276
  
• Stefan Schwendimann:
  A New One-Pass Tableau Calculus for PLTL. 277-292
  
• Klaus Weich:
  Decision Procedures for Intuitionistic Propositional Logic by Program Extraction. 292-306
  

Contributed System Descriptions

• Ian Horrocks:
  The FaCT System. 307-312
  
• Christian Urban:
  Implementation of Proof Search in the Imperative Programming Language Pizza. 313-319
  
• Andreas Wolf:
  p-SETHEO: Strategy Parallelism in Automated Theorem Proving. 320-324
  

Last update Sat May 18 19:50:59 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page