Explaining modal logic proofs

Amy Felty, Greg Hager

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations

Abstract

The authors present a technique for the generation of text explanations for proofs in modal logic. These explanations were generated from structures corresponding to Gentzen style proofs in a modified sequent system. Proofs in this system were represented by a recursive term structure, and natural-language explanations generated by a simple mapping from these term structures to text strings. The authors discuss the X proof system, a tactic-style theorem-proving system for first-order logic with a collection of inference rules corresponding to human-oriented proof techniques. They focus on the extension of X to incorporate proofs in modal logic, and on the different kinds of explanations of modal proofs that can be produced to meet the needs of different users.

Original languageEnglish (US)
Title of host publicationProc 1988 IEEE Int Conf Syst Man Cybern
Editors Anon
Pages177-180
Number of pages4
StatePublished - Dec 1 1988
Externally publishedYes
EventProceedings of the 1988 IEEE International Conference on Systems, Man, and Cybernetics - Beijing/Shenyang, China
Duration: Aug 8 1988Aug 12 1988

Publication series

NameProc 1988 IEEE Int Conf Syst Man Cybern

Other

OtherProceedings of the 1988 IEEE International Conference on Systems, Man, and Cybernetics
CityBeijing/Shenyang, China
Period8/8/888/12/88

ASJC Scopus subject areas

  • General Engineering

Fingerprint

Dive into the research topics of 'Explaining modal logic proofs'. Together they form a unique fingerprint.

Cite this