TY - GEN

T1 - Explaining modal logic proofs

AU - Felty, Amy

AU - Hager, Greg

PY - 1988/12/1

Y1 - 1988/12/1

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

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

UR - http://www.scopus.com/inward/record.url?scp=0024168303&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0024168303&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:0024168303

SN - 7800030393

T3 - Proc 1988 IEEE Int Conf Syst Man Cybern

SP - 177

EP - 180

BT - Proc 1988 IEEE Int Conf Syst Man Cybern

A2 - Anon, null

T2 - Proceedings of the 1988 IEEE International Conference on Systems, Man, and Cybernetics

Y2 - 8 August 1988 through 12 August 1988

ER -