About: MaLeCoP: Machine Learning Connection Prover

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: MaLeCoP: Machine Learning Connection Prover Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
Description	Probabilistic guidance based on learned knowledge is added to the connection tableau calculus and implemented on top of the leanCoP theorem prover, linking it to an external advisor system. In the typical mathematical setting of solving many problems in a large complex theory, learning from successful solutions is then used for guiding theorem proving attempts in the spirit of the MaLARea system. While in MaLARea learning-based axiom selection is done outside unmodified theorem provers, in MaLeCoP the learning-based selection is done inside the prover, and the interaction between learning of knowledge and its application can be much finer. This brings interesting possibilities for further construction and training of self-learning AI mathematical experts on large mathematical libraries, some of which are discussed. The initial implementation is evaluated on the MPTP Challenge large theory benchmark. Probabilistic guidance based on learned knowledge is added to the connection tableau calculus and implemented on top of the leanCoP theorem prover, linking it to an external advisor system. In the typical mathematical setting of solving many problems in a large complex theory, learning from successful solutions is then used for guiding theorem proving attempts in the spirit of the MaLARea system. While in MaLARea learning-based axiom selection is done outside unmodified theorem provers, in MaLeCoP the learning-based selection is done inside the prover, and the interaction between learning of knowledge and its application can be much finer. This brings interesting possibilities for further construction and training of self-learning AI mathematical experts on large mathematical libraries, some of which are discussed. The initial implementation is evaluated on the MPTP Challenge large theory benchmark. (en)
Title	MaLeCoP: Machine Learning Connection Prover MaLeCoP: Machine Learning Connection Prover (en)
skos:prefLabel	MaLeCoP: Machine Learning Connection Prover MaLeCoP: Machine Learning Connection Prover (en)
skos:notation	RIV/68407700:21230/11:00181863!RIV12-MSM-21230___
http://linked.open...avai/riv/aktivita	I Z
http://linked.open...avai/riv/aktivity	I, Z(MSM0021620838), Z(MSM6840770038)
http://linked.open...vai/riv/dodaniDat	2012
http://linked.open...aciTvurceVysledku	Vyskočil, Jiří
http://linked.open.../riv/druhVysledku	D - Článek ve sborníku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	České vysoké učení technické v Praze / Fakulta elektrotechnická
http://linked.open...dnocenehoVysledku	210338
http://linked.open...ai/riv/idVysledku	RIV/68407700:21230/11:00181863
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	automated theorem prover; connection tableaux; machine learning; artificial intelligence (en)
http://linked.open.../riv/klicoveSlovo	automated theorem prover connection tableaux artificial intelligence machine learning
http://linked.open...ontrolniKodProRIV	[4CF2B07DAD46]
http://linked.open...v/mistoKonaniAkce	Bern
http://linked.open...i/riv/mistoVydani	Heidelberg
http://linked.open...i/riv/nazevZdroje	Automated Reasoning with Analytic Tableaux and Related Methods
http://linked.open...in/vavai/riv/obor	JC
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	3 (xsd:int)
http://linked.open...UplatneniVysledku	2011
http://linked.open...iv/tvurceVysledku	Urban, J. Štěpánek, P. Vyskočil, Jiří
http://linked.open...vavai/riv/typAkce	WRD - Světová
http://linked.open.../riv/zahajeniAkce	2011-07-04 (xsd:date)
http://linked.open...n/vavai/riv/zamer	Moderní metody, struktury a systémy informatiky Decision Making and Control for Manufacturing III
issn	0302-9743
number of pages	15 (xsd:int)
http://purl.org/ne...btex#hasPublisher	Springer-Verlag
https://schema.org/isbn	978-3-642-22118-7
http://localhost/t...ganizacniJednotka	21230

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 84 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software