Thumbnail
Access Restriction
Open

Author Nipkow, Tobias
Source CiteSeerX
Content type Text
Publisher Springer
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Church-rosser Proof ♦ Order Logic ♦ Church-rosser Theorem ♦ Fi Reduction ♦ Isabelle Hol ♦ Generic Theorem Prover Isabelle ♦ Untyped Calculus
Description The proofs of the Church-Rosser theorems for fi, j and fi [ j reduction in untyped -calculus are formalized in Isabelle/HOL, an implementation of Higher Order Logic in the generic theorem prover Isabelle.
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 1996-01-01
Journal Journal of Automated Reasoning