Abstract

A tableaux method similiar to the Analytic Tableaux of Raymond Smullyan, First-Order Logic, Springer, New York, 1968, is offered for solving a number of combinatorial satisfiability problems. The exact definition of the problems considered requires the notion of satisfiability in a hypergraph first introduced by Cowen, Hypergraph satisfiability, Reports on Mathematical Logic 25, 113-117, and improved upon by Kolany Satisfiability of hypergraphs, Studia Logica, to appear. The introduction of a general duality principle for hypergraph satisfiability leads to a dual tableau method in each instance.