{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T08:07:38Z","timestamp":1725523658320},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We define a translation that maps higher-order formulas provable in a classical extensional setting to semantically equivalent formulas provable in an intuitionistic intensional setting. For the classical extensional higher-order proof system we define a Henkin-complete tableau calculus. For the intuitionistic intensional higher-order proof system we give a natural deduction calculus. We prove that tableau provability of a formula implies provability of a translated formula in the natural deduction calculus. Implicit in this proof is a method for translating classical extensional tableau refutations into intuitionistic intensional natural deduction proofs.<\/jats:p>","DOI":"10.29007\/8p9q","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T22:59:05Z","timestamp":1516748345000},"page":"27-10","source":"Crossref","is-referenced-by-count":0,"title":["From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction"],"prefix":"10.29007","volume":"14","author":[{"given":"Chad E.","family":"Brown","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christine","family":"Rizkallah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"11545","event":{"name":"PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T22:59:07Z","timestamp":1516748347000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/Ps"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/8p9q","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}