Encoding Labelled Non-Classical Logics in Isabelle

  • Luca Viganò


We have used the generic theorem prover Isabelle [181] to implement the non-classical logis we presented. The logical basis of Isabelle is a natural deduction presentation of minimal implicational predicate logic with universal quantification over all higher-types [179].1 We call this metalogic Meta, and to prevent object/meta confusion we use Λ to represent Meta’s universal quantifier and ⇒ for implication.


Normal Form Logical Operator Universal Quantification Concrete Syntax Proof State 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media Dordrecht 2000

Authors and Affiliations

  • Luca Viganò
    • 1
  1. 1.Institut für InformatikAlbert-Ludwigs-Universität FreiburgFreiburg im BreisgauGermany

Personalised recommendations