Skip navigation
Skip navigation

Computational Natural Deduction

Keronen, Seppo R.

Description

The formalization of the notion of a logically sound argument as a natural deduction proof offers the prospect of a computer program capable of constructing such arguments for conclusions of interest. We present a constructive definition for a new subclass of natural deduction proofs, called atomic normal form (ANF) proofs. A natural deduction proof is readily understood as an argument leading from a set of premisses, by way of simple principles of reasoning, to the conclusion of interest....[Show more]

dc.contributor.authorKeronen, Seppo R.
dc.date.accessioned2012-08-30T07:17:33Z
dc.identifier.otherb18286537
dc.identifier.urihttp://hdl.handle.net/1885/9243
dc.description.abstractThe formalization of the notion of a logically sound argument as a natural deduction proof offers the prospect of a computer program capable of constructing such arguments for conclusions of interest. We present a constructive definition for a new subclass of natural deduction proofs, called atomic normal form (ANF) proofs. A natural deduction proof is readily understood as an argument leading from a set of premisses, by way of simple principles of reasoning, to the conclusion of interest. ANF extends this explanative power of natural deduction. The very detailed steps of the argument are replaced by derived rules of inference, each of which is justified by a particular input formula. ANF constitutes a proof theoretically well motivated normal form for natural deduction. Computational techniques developed for resolution refutation based systems are directly applicable to the task of constructing ANF proofs. We analyse a range of languages in this framework, extending from the simple Horn language to the full classical calculus. This analysis is applied to provide a natural deduction based account for existing logic programming languages, and to extend current logic programming implementation techniques towards more expressive languages. We consider the visualization of proofs, failure demonstrations, search spaces and the proof search process. Such visualization can be used for the purposes of explanation and to gain an understanding of the proof search process. We propose introspection based architecture for problem solvers based on natural deduction. The architecture offers a logic based meta language to overcome the combinatorial and other practical problems faced by the problem solver.
dc.language.isoen_AU
dc.subjectcomputational logic
dc.subjectnatural deduction
dc.subjectlogic programming
dc.titleComputational Natural Deduction
dc.typeThesis (PhD)
local.contributor.supervisorStanton, Robin
dcterms.valid1992
local.description.notesSupervisor: Prof Robin Stanton
local.description.refereedYes
local.type.degreeDoctor of Philosophy (PhD)
dc.date.issued1991
local.contributor.affiliationDepartment of Computer Science
local.request.emaillibrary.digital-thesis@anu.edu.au
local.request.nameDigital Theses
local.identifier.doi10.25911/5d78dc1842b02
local.mintdoimint
CollectionsOpen Access Theses

Download

File Description SizeFormat Image
04Chapter4-7_keronen.pdf4.7 MBAdobe PDFThumbnail
03Chapte1-3_keronen.pdf3.51 MBAdobe PDFThumbnail
01Front_keronen.pdfFront Matter_FOR ACCESS TO THIS THESIS PLEASE GO TO http://anulib.anu.edu.au/about/collections/theses_externalaccess.html751.84 kBAdobe PDFThumbnail
Keronen Thesis 2004.pdf8.93 MBAdobe PDFThumbnail


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  17 November 2022/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator