Decision Problems and Some Solutions
Viewed as a collection of sentences, any first-order theory of sets is recursively enumerable: this is an advantage ensuing from the axiomatic method. To restate it, a list of all sentences provable in the theory can be generated through an automatic (infinite) process. Moreover, a reliable certification of theoremhood (that is, a formal derivation from the axioms of the theory) can come along with each sentence in the list.
KeywordsDecision Problem Boolean Algebra Free Variable Conjunctive Normal Form Satisfiability Problem
Unable to display preview. Download preview PDF.