Mechanizing relevant logics with HOL

DOI10.1007/BFB0055151MaRDI QIDQ4247086zbMATH OpenFDO

Authors Hajime Sawamura, Daisaku Asanuma

Publication date 13 December 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0055151

zbMATH Keywords

higher-order representationHOLinteractive theorem proverpossible worlds semanticsrelevant logics

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Recommendations

• Relevant logics: from semantics to proof systems
• scientific article; zbMATH DE number 2042611
• Relational proof system for relevant logics
• Algorithms for relevant logic

Cited in

(1)

• scientific article; zbMATH DE number 1231561 (Why is no real title available?)

Describes a project that uses

Uses Software

• Isabelle
• HOL
• EUODHILOS

This page was built for publication: Mechanizing relevant logics with HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4247086)