Algebraic proof assistants in HOL

Autor:	Rix Groenboom, Jan Tijmen Udding, Chris Hendriks, Indra Polak, Jan Terlouw
Rok vydání:	1995
Předmět:	Algebraic laws Discrete mathematics TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Proof assistant Internal function Calculus HOL Granularity Algebraic number Mathematics
Zdroj:	Lecture Notes in Computer Science ISBN: 9783540601173 MPC
DOI:	10.1007/3-540-60117-1_17
Popis:	We explore several ways to formalize the algebraic laws of CSP-like languages in HOL. The intent of the paper is to show how HOL can be tailored to acting as a proof assistant. The emphasis is therefore on the consequences of various choices to be made during the formalization for writing tactics. We end up with a proof assistant that allows a user to make steps of the granularity of an algebraic law. It is not the purpose of this paper to show in HOL that the algebraic laws of some CSP-like language are sound; the purpose is to show how HOL can be used to apply the algebraic laws and act as a rewrite system.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::8b6d52ce94ebc2660e31353db86bb5a7 https://doi.org/10.1007/3-540-60117-1_17 Zobrazit plný text záznamu