Thumbnail
Access Restriction
Open

Author Aspinall, David ♦ Denney, Ewen
Source CiteSeerX
Content type Text
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Interaction Point ♦ Tactical Combinators ♦ Large Tree ♦ Faulty Tactic Proof ♦ Process Map ♦ Successful Tactic Proof ♦ Formal Text ♦ Ordinary Proof Tree ♦ Unified Notion ♦ Hitac Program ♦ Labelled Hierarchical Nesting ♦ Primitive Logical Inference ♦ Hierarchical Proof ♦ Possible Implementation ♦ Explicit Connection ♦ Small-step Semantics ♦ Debugging Tool ♦ Proof Tree ♦ Construction Process ♦ Search Procedure ♦ Popular Tacti-cal Theorem Provers ♦ Proof State ♦ Foundational Tactic Language Hitac ♦ Generic Setting ♦ High-level Human Input ♦ Intended Meaning ♦ Typical Example ♦ Big-step Semantics ♦ Fully-checked Mechanical Proof ♦ Small-step Operational Semantics ♦ Construct Valid Proof
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 Institution Mathematics in Computer Science