Technical Report TR-ARP-6-95

Automated Reasoning Project
Research School of Information Sciences and Engineering
and Centre for Information Science Research
Australian National University

April, 26, 1995

A UNIFORM DISPLAY SYSTEM FOR

INTUITIONISTIC AND DUAL

INTUITIONISTIC LOGIC

Rajeev Gor?e

Abstract We give a way to display" propositional intuitionistic and dual-intuitionistic logic in one uniform setting. We show how the usual singletons on the right" restriction of Gentzen's LJ, and the dual singletons on the left" restriction can be mimicked in Display Logic. The resulting Display System ffi JDJ captures a hybrid logic that permits reasoning with partial and paraconsistent knowledge since it contains two negations : and ? with the following properties: A _ :A is not a theorem; A^ ? A is not a contradiction; A ^ :A is a contradiction; and A_ ? A is a theorem. We then show how to obtain a Display system for Classical Logic by the addition of structural rules only.

Keywords: logical and mathematical models for AI, paraconsistent logics, intuitionistic logic, hybrid logics, automated reasoning.