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, EztrueEzfalseEzp, 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 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, EztrueEzfalseEzp, and a counterexample of its converse, EzpEztrueEzfalse. The first proof uses the Shannon theorem, Ezp ≡ (pEztrue) ∨ (∼pEzfalse); the latter does not.

This document is currently not available here.

Share

COinS
 
Nov 17th, 10:00 AM Nov 17th, 10:15 AM

A Theorem for Case Analysis

C302

This paper uses the equational deductive system to present a new theorem, EztrueEzfalseEzp, 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 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.