A generic graphic framework for combining inference tools and editing proofs and formulae

DOI10.1006/JSCO.1995.1013MaRDI QIDQ1895412zbMATH OpenOpenAlexFDO

Authors Ricardo Caferra, Michel Herment

Publication date 11 April 1996

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1006/jsco.1995.1013

zbMATH Keywords

editinginference toolscalculus of constructionchecking proofs

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 500942
• scientific article; zbMATH DE number 1629953
• scientific article; zbMATH DE number 1024410
• A graphical user interface for formal proofs in geometry
• The foundation of a generic theorem prover

Cited in

(4)

• Geometry machines: from AI to SMC
• MikiBeta : A General GUI Library for Visualizing Proof Trees
• A Shell for Generic Interactive Proof Search
• scientific article; zbMATH DE number 500942 (Why is no real title available?)

Describes a project that uses

Uses Software

• Nuprl
• OTTER
• Mathematica
• Coq

This page was built for publication: A generic graphic framework for combining inference tools and editing proofs and formulae

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