#### Presentation Title

A Theorem for Case Analysis

#### Faculty Mentor

Stan Warford

#### Start Date

17-11-2018 10:00 AM

#### End Date

17-11-2018 10:15 AM

#### Location

C302

#### Session

Oral 2

#### Type of Presentation

Oral Talk

#### Subject Area

engineering_computer_science

#### Abstract

This paper uses the equational deductive system to present a new theorem, *E ^{z}_{true}* ∧

*E*⇒

^{z}_{false}*E*, which is used in proofs by case analysis. The equational system, developed by Dijkstra and Scholten and extended by Gries and Schneider in their text

^{z}_{p}*A Logical Approach to Discrete Math*, is based on only four inference rules Substitution, Leibniz, Equanimity, and Transitivity. Inference rules in the older Hilbert-style systems, notably modus ponens, appear as theorems in this equational deductive system, which is used to prove algorithm correctness in computer science. The theorem presented in this paper exists only as a metatheorem in the Gries and Schneider text. Two proofs of the theorem are presented; one applies the Shannon theorem. Both of these proofs avoid the proof technique of assuming the antecedent (which would be illicit given the precedence of theorems over proof technique metatheorems). Finally, this paper gives a counterexample for the converse of the new theorem, establishing that the implication in the theorem cannot be replaced with equivalence.

#### Summary of research results to be presented

The research results to be presented are two proofs of the theorem, *E ^{z}_{true}* ∧

*E*⇒

^{z}_{false}*E*and a counterexample of its converse,

^{z}_{p,}*E*⇒

^{z}_{p}*E*∧

^{z}_{true}*E*. The first proof uses the Shannon theorem,

^{z}_{false}*E*≡ (

^{z}_{p}*p*∧

*E*) ∨ (∼

^{z}_{true}*p*∧

*E*); the latter does not.

^{z}_{false}A Theorem for Case Analysis

C302

This paper uses the equational deductive system to present a new theorem, *E ^{z}_{true}* ∧

*E*⇒

^{z}_{false}*E*, which is used in proofs by case analysis. The equational system, developed by Dijkstra and Scholten and extended by Gries and Schneider in their text

^{z}_{p}*A Logical Approach to Discrete Math*, is based on only four inference rules Substitution, Leibniz, Equanimity, and Transitivity. Inference rules in the older Hilbert-style systems, notably modus ponens, appear as theorems in this equational deductive system, which is used to prove algorithm correctness in computer science. The theorem presented in this paper exists only as a metatheorem in the Gries and Schneider text. Two proofs of the theorem are presented; one applies the Shannon theorem. Both of these proofs avoid the proof technique of assuming the antecedent (which would be illicit given the precedence of theorems over proof technique metatheorems). Finally, this paper gives a counterexample for the converse of the new theorem, establishing that the implication in the theorem cannot be replaced with equivalence.