Article contents
A conjunctive normal form for S3.5
Published online by Cambridge University Press: 12 March 2014
Extract
In this note we sketch a decision procedure for S3.51 based on reduction to conjunctive normal form. Using the following theorem of S3.5: and its dual for M over a conjunction, any formula can be reduced by standard methods (as in S52) to a conjunction of disjunctions of the form where Í is (p ⊃ p), 0 is ∼(p ⊃ p) and α — λ are all PC-wffs (i.e. they contain no modal operators).
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 1969
References
- 1
- Cited by