Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange

Result code in 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>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange

Original language description

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.

Czech name

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

Czech description

Zvaná přednáška a článek na workshopech KEAPPA a IWIL při konferenci LPAR'2008. Článek podává přehled o existujícím propojení mezi projektem Mizar pro formalizaci matematiky, a nástroji pro automatické uvažování (a zejména automatické dokazování vět). Vysvětluje motivaci pro tuto práci, podává přehled překladových metod a přehled projektů a experimentů založených na tomto propojení. Dále diskutuje možné budoucí projekty a směry výzkumu v této oblasti.

Type

A - Audiovisual production

CEP classification

JD - Use of computers, robotics and its application

OECD FORD branch

—

Project

—

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2008

Confidentiality

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

ISBN

—

Place of publication

—

Publisher/client name

—

Version

—

Carrier ID

—