Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX'97, Pont-a-Mousson, France, May 13-16, 1997 Proceedings

by Didier Galmiche (Editor)

Overview

This book constitutes the refereed proceedings of the International Conference on Analytic Tableaux and Related Methods, TABLEAUX'97, held in Pont-a-Mousson, France, in May 1997.

The volume presents 22 revised full papers selected from a total of 49 submissions. Also included are two invited papers and two system descriptions. The volume covers the whole spectrum of tableaux-based theorem proving and its applications including theoretical foundations, methodological issues, implementation techniques, and system development. Besides classical logics, among the logics dealt with are modal, intuitionistic, many-valued, and temporal logic.

Product Details

ISBN-13:	9783540629207
Publisher:	Springer Berlin Heidelberg
Publication date:	05/29/1997
Series:	Lecture Notes in Computer Science , #1227
Edition description:	1997
Pages:	380
Product dimensions:	6.10(w) x 9.25(h) x 0.36(d)

Table of Contents

MGTP: A model generation theorem prover — Its advanced features and applications —.- Three faces of natural deduction.- Tableaux for logic programming with strong negation.- Generalized tableau systems for intermediate propositional logics.- Lean induction principles for tableaux.- Tableaux for diagnosis applications.- Free variable tableaux for propositional modal logics.- A sequent calculus for skeptical Default Logic.- A fast saturation strategy for set-theoretic tableaux.- Hintikka multiplicities in matrix decision methods for some propositional modal logics.- Automated natural deduction prover and experiments.- Non-elementary speed-ups in proof length by different variants of classical analytic calculi.- Ordered tableaux: Extensions and applications.- Two loop detection mechanisms: A comparison.- Subgoal alternation in model elimination.- Projection: A unification procedure for tableaux in Conceptual Graphs.- On quasitautologies.- Tableaux methods for access control in distributed systems.- Proving correctness of labeled transition systems by semantic tableaux.- Tableau methods for PA-processes.- A tableau proof system for a mazurkiewicz trace logic with fixpoints.- ileanTAP: An intuitionistic theorem prover.- Simplifying and generalizing formulae in tableaux. Pruning the search space and building models.- A framework for using knowledge in tableau proofs.- A sequent calculus for reasoning in four-valued Description Logics.- Tableaux for functional dependencies and independencies.