The Alf proof editor and its proof engine

DOI10.1007/3-540-58085-9_78MaRDI QIDQ6083695zbMATH OpenOpenAlexFDO

Authors Lena Magnusson, Bengt Nordström

Publication date 8 December 2023

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

Full work available at URL https://doi.org/10.1007/3-540-58085-9_78

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 978243
• scientific article; zbMATH DE number 4072441
• The Theorema Environment for Interactive Proof Development
• scientific article; zbMATH DE number 1696759
• scientific article; zbMATH DE number 500942
• A semi-algorithm for algebraic implementation proofs
• Artificial Intelligence and Symbolic Computation

Cites work

• A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
• A unification algorithm for typed -calculus
• Edinburgh LCF. A mechanized logic of computation
• Higher-order unification with dependent function types
• scientific article; zbMATH DE number 4058907 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 65534 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• The calculus of constructions

Cited in

(5)

• Inductive beluga: programming proofs
• A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (System Description)
• Set theory, higher order logic or both?
• Function definition in higher-order logic
• A mechanisation of computability theory in HOL

This page was built for publication: The Alf proof editor and its proof engine

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