The Use of Proof Plans for Normalization

Autor:	Alan Bundy
Přispěvatelé:	Boyer, R. S.
Rok vydání:	1991
Předmět:	Normalization (statistics) Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Theoretical computer science Proof complexity Conjunctive normal form Algorithm Mathematics
Zdroj:	Automated Reasoning Series ISBN: 9789401055420 Automated Reasoning: Essays in Honor of Woody Bledsoe Bundy, A 1991, The Use of Proof Plans for Normalization . in R S Boyer (ed.), Essays in Honour of Woody Bledsoe . Kluwer Academic Publishers .
Popis:	We propose using proof plans to implement expression normalizers in automatic theorem proving. We outline some general-purpose proof plans and show how these can be combined in various ways to yield some standard normalizers. We claim that using proof plans facilitates the flexible application of these normalizers so that they can interact with the theorem prover in which they are embedded. We intend to extend this technique to decision procedures.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::42ba8d1d8d3b93ffb8dc932527fe38a6 https://doi.org/10.1007/978-94-011-3488-0_7 Zobrazit plný text záznamu