Presentation Title

A Quadrotomy for Partial Orders

Faculty Mentor

Stan Warford

Start Date

23-11-2019 10:30 AM

End Date

23-11-2019 10:45 AM

Location

Markstein 208

Session

oral 2

Type of Presentation

Oral Talk

Subject Area

engineering_computer_science

Abstract

This paper uses a calculational system to formally prove a quadrotomy for partial orders ⪯, which states that any element x of the partial order must be related to any other element y by exactly one of (a) x ≺ y, (b) x = y, (c) y ≺ x, or (d) incomp(x,y), where ≺ is the reflexive reduction of ⪯ and incomp(x, y) is defined as incomp(x, y) ≡ ¬(x ⪯ y) ∧ ¬(y ⪯ x). The calculational 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 calculational deductive system, which is used to prove algorithm correctness in computer science. The theorem presented in this paper is a generalization of the trichotomy theorem for integers proved by Gries and Schneider, which states that any integer n must be related to any other integer m by exactly one of (a) n < m, (b) n = m, or (c) m < n.

This document is currently not available here.

Share

COinS
 
Nov 23rd, 10:30 AM Nov 23rd, 10:45 AM

A Quadrotomy for Partial Orders

Markstein 208

This paper uses a calculational system to formally prove a quadrotomy for partial orders ⪯, which states that any element x of the partial order must be related to any other element y by exactly one of (a) x ≺ y, (b) x = y, (c) y ≺ x, or (d) incomp(x,y), where ≺ is the reflexive reduction of ⪯ and incomp(x, y) is defined as incomp(x, y) ≡ ¬(x ⪯ y) ∧ ¬(y ⪯ x). The calculational 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 calculational deductive system, which is used to prove algorithm correctness in computer science. The theorem presented in this paper is a generalization of the trichotomy theorem for integers proved by Gries and Schneider, which states that any integer n must be related to any other integer m by exactly one of (a) n < m, (b) n = m, or (c) m < n.