Automatické dokazování pro Mizar: umělá inteligence pomocí výměny znalostí

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F08%3A00100205" target="_blank" >RIV/00216208:11320/08:00100205 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange

Popis výsledku v původním jazyce

This paper gives an overview of the existing link between the Mizar projekt for formalization of mathematics and Automated Reasonig tols (mainly the Automater Theorem Provers (ATPs)). It explains the motovation for this work, gives an overview of the translation method, discusses the projects and works that are based on it, and possible future projects and directions.

Název v anglickém jazyce

Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange

Popis výsledku anglicky

This paper gives an overview of the existing link between the Mizar projekt for formalization of mathematics and Automated Reasonig tols (mainly the Automater Theorem Provers (ATPs)). It explains the motovation for this work, gives an overview of the translation method, discusses the projects and works that are based on it, and possible future projects and directions.

Druh

A - Audiovizuální tvorba

CEP obor

JD - Využití počítačů, robotika a její aplikace

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2008

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ů

ISBN

—

Místo vydání

—

Název nakladatele resp. objednatele

—

Verze

—

Identifikační číslo nosiče

—