A practical implementation of simple consequence relations using inductive definitions

DOI10.1007/3-540-63104-6_31MaRDI QIDQ5234714zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• scientific article; zbMATH DE number 2110615
• Using typed lambda calculus to implement formal systems on a machine
• scientific article; zbMATH DE number 65531
• Functional and Logic Programming
• Logical frameworks

Cites work

• scientific article; zbMATH DE number 4180832 (Why is no real title available?)
• scientific article; zbMATH DE number 4033738 (Why is no real title available?)
• A framework for defining logics
• A theory of binding structures and applications to rewriting
• Axiomatic System, Deduction and Implication
• Isabelle. A generic theorem prover
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Simple consequence relations
• Structuring metatheory on inductive definitions
• The foundation of a generic theorem prover
• Using typed lambda calculus to implement formal systems on a machine

Describes a project that uses

Uses Software

• Automath
• Isabelle

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

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