Theorem Proving with Analytic Tableaux and Related Methods: 4th International Workshop, TABLEAUX-95, Schloß Rheinfels, St. Goar, Germany, May 7 - 10, 1995. Proceedings

Issues in theorem proving based on the connection method.- Rigid E-unification simplified.- Generating finite counter examples with semantic tableaux.- Semantic tableaus for inheritance nets.- Using connection method in modal Some advantages.- Labelled tableaux for multi-modal logics.- Refutation systems for prepositional modal logics.- On transforming intuitionistic matrix proofs into standard-sequent proofs.- A connection based proof method for intuitionistic logic.- Tableau for intuitionistic predicate logic as metatheory.- Model building and interactive theory discovery.- Link deletion in model elimination.- Specifications of inference rules and their automatic translation.- Constraint model elimination and a PTTP-implementation.- Non-elementary speedups between different versions of tableaux.- Syntactic reduction of predicate tableaux to propositional tableaux.- Classical Lambek logic.- Linear logic with Pruning the proof search tree.- Linear analytic tableaux.- Higher-order tableaux.- Propositional logics on the computer.- Yet another proof assistant & automated pedagogic tool.- Using the theorem prover SETHEO for verifying the development of a communication protocol in FOCUS -A Case Study-.