This HTML5 document contains 42 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n5http://linked.opendata.cz/ontology/domain/vavai/riv/typAkce/
dctermshttp://purl.org/dc/terms/
n15http://purl.org/net/nknouf/ns/bibtex#
n10http://localhost/temp/predkladatel/
n13http://linked.opendata.cz/resource/domain/vavai/riv/tvurce/
n20http://linked.opendata.cz/ontology/domain/vavai/
n21https://schema.org/
n18http://linked.opendata.cz/resource/domain/vavai/zamer/
shttp://schema.org/
skoshttp://www.w3.org/2004/02/skos/core#
n17http://linked.opendata.cz/resource/domain/vavai/vysledek/RIV%2F00216208%3A11320%2F07%3A00206156%21RIV10-MSM-11320___/
n3http://linked.opendata.cz/ontology/domain/vavai/riv/
n2http://linked.opendata.cz/resource/domain/vavai/vysledek/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n9http://linked.opendata.cz/ontology/domain/vavai/riv/klicoveSlovo/
n16http://linked.opendata.cz/ontology/domain/vavai/riv/duvernostUdaju/
xsdhhttp://www.w3.org/2001/XMLSchema#
n19http://linked.opendata.cz/ontology/domain/vavai/riv/aktivita/
n4http://linked.opendata.cz/ontology/domain/vavai/riv/jazykVysledku/
n12http://linked.opendata.cz/ontology/domain/vavai/riv/obor/
n8http://linked.opendata.cz/ontology/domain/vavai/riv/druhVysledku/
n11http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:RIV%2F00216208%3A11320%2F07%3A00206156%21RIV10-MSM-11320___
rdf:type
skos:Concept n20:Vysledek
dcterms:description
Mizar is a proof assistant used for formalization and mechanical verification of mathematics. The main use of Mizar is in the development of the Mizar Mathematical Library (MML), in which proofs are verified by the Mizar proof checker. The Mizar proof checker has a quite complex implementation, and also lacks the ability to print out detailed atomic proof steps in a format that is easy to verify by an independent proof-checking tool. This can raise concerns about the correctness of the MML. This paper describes how a Mizar-to-ATP translation (the MPTP system); ATP verification tools (the GDV system), and Automated Theorem Proving (ATP) systems, have been used for an independent cross-verification of a part of the MML. Mizar is a proof assistant used for formalization and mechanical verification of mathematics. The main use of Mizar is in the development of the Mizar Mathematical Library (MML), in which proofs are verified by the Mizar proof checker. The Mizar proof checker has a quite complex implementation, and also lacks the ability to print out detailed atomic proof steps in a format that is easy to verify by an independent proof-checking tool. This can raise concerns about the correctness of the MML. This paper describes how a Mizar-to-ATP translation (the MPTP system); ATP verification tools (the GDV system), and Automated Theorem Proving (ATP) systems, have been used for an independent cross-verification of a part of the MML.
dcterms:title
ATP Cross-Verification of the Mizar MPTP Challenge Problems ATP Cross-Verification of the Mizar MPTP Challenge Problems
skos:prefLabel
ATP Cross-Verification of the Mizar MPTP Challenge Problems ATP Cross-Verification of the Mizar MPTP Challenge Problems
skos:notation
RIV/00216208:11320/07:00206156!RIV10-MSM-11320___
n3:aktivita
n19:Z
n3:aktivity
Z(MSM0021620838)
n3:dodaniDat
n11:2010
n3:domaciTvurceVysledku
n13:5283434
n3:druhVysledku
n8:D
n3:duvernostUdaju
n16:S
n3:entitaPredkladatele
n17:predkladatel
n3:idSjednocenehoVysledku
411007
n3:idVysledku
RIV/00216208:11320/07:00206156
n3:jazykVysledku
n4:eng
n3:klicovaSlova
Cross-Verification; Mizar; Challenge; Problems
n3:klicoveSlovo
n9:Mizar n9:Cross-Verification n9:Challenge n9:Problems
n3:kontrolniKodProRIV
[4D75D652DFC4]
n3:mistoKonaniAkce
Berlin
n3:mistoVydani
Berlin
n3:nazevZdroje
Logic for Programming, Artificial Intelligence, and Reasoning
n3:obor
n12:JC
n3:pocetDomacichTvurcuVysledku
1
n3:pocetTvurcuVysledku
2
n3:rokUplatneniVysledku
n11:2007
n3:tvurceVysledku
Urban, Josef Sutcliffe, Geoff
n3:typAkce
n5:WRD
n3:wos
000251785100039
n3:zahajeniAkce
2007-01-01+01:00
n3:zamer
n18:MSM0021620838
s:numberOfPages
15
n15:hasPublisher
Springer-Verlag
n21:isbn
978-3-540-75558-6
n10:organizacniJednotka
11320