Isabelle-91

e introducing the types and constants of the logic, i.e. its abstract syntax, and axioms describing the inference rules. As a tiny example, consider the following definition of minimal logic. Min = types form consts - : form (form form) [[ ]] : form prop rules ([[P]] = [[Q]]) = [[P - Q]] [[P - Q]] = [[P]] = [[Q]] Min introduces the type form (of object-formulae) and the infix constant - (for objectimplication). The constant [[ ]] maps form to the predefined type prop of meta-logic propositions. The proposition [[P]] should be read as "the formula P is true"; we usually distinguish object-level formulae (form) from meta-level formulae (prop). In practice the brackets can be dropped; parser and pretty-printer take care of such matters. The two rules for minimal logic are typical natural deduction rules for implication

• Type: Conference
• Year: 1992
• Where: CADE
• Authors: Tobias Nipkow, Lawrence C. Paulson
• Keywords: CADE 1992, Form Prop Rules, Logical Reasoning, Minimal Logic, Types Form Consts