Uniform Provability in Classical Logic

Details Uniform Provability in Classical Logic Uniform Provability in Classical Logic

1998-09-10

arxiv.org/abs/cs/9809014v1

Journal of Logic and Computation, Vol 8, No 96-15, pp 209-229, 1998

Computer Science

Logic in Computer Science

23 pages

Scientific paper

Uniform proofs are sequent calculus proofs with the following characteristic: the last step in the derivation of a complex formula at any stage in the proof is always the introduction of the top-level logical symbol of that formula. We investigate the relevance of this uniform proof notion to structuring proof search in classical logic. A logical language in whose context provability is equivalent to uniform provability admits of a goal-directed proof procedure that interprets logical symbols as search directives whose meanings are given by the corresponding inference rules. While this uniform provability property does not hold directly of classical logic, we show that it holds of a fragment of it that only excludes essentially positive occurrences of universal quantifiers under a modest, sound, modification to the set of assumptions: the addition to them of the negation of the formula being proved. We further note that all uses of the added formula can be factored into certain derived rules. The resulting proof system and the uniform provability property that holds of it are used to outline a proof procedure for classical logic. An interesting aspect of this proof procedure is that it incorporates within it previously proposed mechanisms for dealing with disjunctive information in assumptions and for handling hypotheticals. Our analysis sheds light on the relationship between these mechanisms and the notion of uniform proofs.

Affiliated with

Also associated with

No associations

Rating

Uniform Provability in Classical Logic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Uniform Provability in Classical Logic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Uniform Provability in Classical Logic will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-230150