A practical implementation of simple consequence relations using inductive definitions

DOI10.1007/3-540-63104-6_31zbMath1430.68417OpenAlexW1544121389MaRDI QIDQ5234714

Seán Matthews

Publication date: 1 October 2019

Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-63104-6_31

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Isabelle
• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• A theory of binding structures and applications to rewriting
• Using typed lambda calculus to implement formal systems on a machine
• Simple consequence relations
• Isabelle. A generic theorem prover
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• The foundation of a generic theorem prover
• Axiomatic System, Deduction and Implication
• A framework for defining logics
• Structuring metatheory on inductive definitions

This page was built for publication: A practical implementation of simple consequence relations using inductive definitions