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 -