Tableau-based theorem proving for a conditional logic
Christine Groeneboer · Summit (Simon Fraser University) · 1987
This thesis presents a tableau-based approach to theorem-proving for a conditional logic.Conditional logics are those logics concerned with statements of the form "if a then P." A nth-functional semantics for the material conditional a 3 P is that a 2 P is equivalent by definition to a Vj3.Then whenever a is true, so is j3.For example, penguin(x) 3 bird(x) is true because for every x such that x is a penguin, x is a bird.However, exception-admitting conditional knowledge such as knowledge about laws of nature, natural kinds, and properties of kinds is not readily formalized with material conditionals.Many of the properties of material conditionals fail for such "natural conditionals," e.g., transitivity: penguins are birds, birds normally fly, but it is not the case that penguins normally fly.Logic N is a conditional logic devised to represent the relation between natural kinds and properties of kinds.A variably strict conditional operator "*" is added to propositional logic.Informally, "a + P" means "in the normal course of events, if a then p" or "all other things being equal, if a then P."A tableau-based approach to theorem-proving for conditional logic N is presented A tableau represents an attempt to construct a model in which +o is satisfiable in order to prove o.If such a model can be constructed, o is invalid.Otherwise such a model is shown to be impossible to construct, and o is therefore valid.This approach is based on semantic diagrams for modal logics and temporal logics.The method is shown to be sound and complete and has been implemented in program Validate, an automated theorem-prover for conditional logic N.