Static learning for an adaptative theorem prover

Autor:	Jacques Nicolas, Catherine Belleannée
Rok vydání:	1991
Předmět:	Set (abstract data type) Automated theorem proving Theoretical computer science Fundamental theorem Proof calculus Sequent calculus Representation (mathematics) Rule of inference Algorithm Mathematics Domain (software engineering)
Zdroj:	Lecture Notes in Computer Science ISBN: 9783540538165 EWSL
DOI:	10.1007/bfb0017022
Popis:	An adaptative theorem prover is a system able to modify its current set of inference rules in order to improve its performance on a specific domain. We address here the issue of the generation of inference rules, without considering the selection and deletion issues. We especially develop the treatment of repeating events within a proof. We specify a general representation for objects to be learned in this framework, that is macro-connectives and macro-inference-rules and show how they may be generated from the primitive set of inference rules. Our main contribution consists to show that a form of analytical, static learning, is possible in this domain.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::d55a0f8b925ac10262e83d36f2a3d936 https://doi.org/10.1007/bfb0017022 Zobrazit plný text záznamu