Translating SUMO-K to Higher-Order Set Theory

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F23%3A00372139" target="_blank" >RIV/68407700:21730/23:00372139 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1007/978-3-031-43369-6_14" target="_blank" >https://doi.org/10.1007/978-3-031-43369-6_14</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-43369-6_14" target="_blank" >10.1007/978-3-031-43369-6_14</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Translating SUMO-K to Higher-Order Set Theory

Popis výsledku v původním jazyce

We describe a translation from a fragment of SUMO (SUMO-K) into higher-order set theory. The translation provides a formal semantics for portions of SUMO which are beyond first-order and which have previously only had an informal interpretation. It also for the first time embeds a large common-sense ontology into an interactive theorem proving system. We further extend our previous work in finding contradictions in SUMO from first-order constructs to include a portion of SUMO’s higher-order constructs. Finally, using the translation, we can create problems that can be proven using higher-order interactive and automated theorem provers. This is tested in several systems and used to form a corpus of higher-order common-sense reasoning problems.

Název v anglickém jazyce

Translating SUMO-K to Higher-Order Set Theory

Popis výsledku anglicky

We describe a translation from a fragment of SUMO (SUMO-K) into higher-order set theory. The translation provides a formal semantics for portions of SUMO which are beyond first-order and which have previously only had an informal interpretation. It also for the first time embeds a large common-sense ontology into an interactive theorem proving system. We further extend our previous work in finding contradictions in SUMO from first-order constructs to include a portion of SUMO’s higher-order constructs. Finally, using the translation, we can create problems that can be proven using higher-order interactive and automated theorem provers. This is tested in several systems and used to form a corpus of higher-order common-sense reasoning problems.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2023

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Frontiers of Combining Systems

ISBN

978-3-031-43368-9

ISSN

2945-9133

e-ISSN

1611-3349

Počet stran výsledku

20

Strana od-do

255-274

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Praha

Datum konání akce

20. 9. 2023

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001156327100014