An overview of the Tecton proof system
From MaRDI portal
Recommendations
Cites work
- A higher-order implementation of rewriting
- A Practical Decision Procedure for Arithmetic with Function Symbols
- An axiomatic basis for computer programming
- An overview of the Tecton proof system
- Edinburgh LCF. A mechanized logic of computation
- scientific article; zbMATH DE number 4074541 (Why is no real title available?)
- scientific article; zbMATH DE number 4112064 (Why is no real title available?)
- scientific article; zbMATH DE number 3684928 (Why is no real title available?)
- scientific article; zbMATH DE number 44187 (Why is no real title available?)
- scientific article; zbMATH DE number 193479 (Why is no real title available?)
- scientific article; zbMATH DE number 517385 (Why is no real title available?)
- scientific article; zbMATH DE number 3804893 (Why is no real title available?)
- Report on the Larch shared language
- Simplification by Cooperating Decision Procedures
- Termination of rewriting
Cited in
(11)- Gordon's computer: A hardware verification case study in OBJ3
- An overview of the Tecton proof system
- Constraint contextual rewriting.
- Automatic proofs by induction in theories without constructors
- An approach to literate and structured formal developments
- New uses of linear arithmetic in automated theorem proving by induction
- System description: GAPT 2.0
- Tecton
- Refactoring proofs with Tactician
- \textit{Mollusc}: a general proof-development shell for sequent-based logics
- TPS: A hybrid automatic-interactive system for developing proofs
This page was built for publication: An overview of the Tecton proof system
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1341710)
