#### 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.

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.