Structuring metatheory on inductive definitions

DOI10.1007/3-540-61511-3_79zbMath1412.68205OpenAlexW1536073213MaRDI QIDQ4647512

Seán Matthews, David A. Basin

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_79

zbMATH Keywords

modal logicnatural deductionproof systemtheorem proverobject logic

Mathematics Subject Classification ID

Related Items (1)

A practical implementation of simple consequence relations using inductive definitions

Uses Software

• Isabelle
• ML
• HOL
• LCF

Cites Work

• Using typed lambda calculus to implement formal systems on a machine
• Modal logic as metalogic
• Isabelle. A generic theorem prover
• Edinburgh LCF. A mechanized logic of computation
• A framework for defining logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Structuring metatheory on inductive definitions