An overview of the Tecton proof system

DOI10.1016/0304-3975(94)90192-9zbMath0938.68823OpenAlexW2060173806MaRDI QIDQ1341710

V. Pereyra

Publication date: 15 June 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(94)90192-9

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items

Gordon's computer: A hardware verification case study in OBJ3, An overview of the Tecton proof system, An approach to literate and structured formal developments, New uses of linear arithmetic in automated theorem proving by induction, Constraint contextual rewriting., Tecton, Automatic proofs by induction in theories without constructors

Uses Software

• LARCH
• PVS
• Nuprl
• NQTHM
• LEGO
• RRL
• AFFIRM
• Cambridge LCF

Cites Work

• A higher-order implementation of rewriting
• Report on the Larch shared language
• Termination of rewriting
• An overview of the Tecton proof system
• Edinburgh LCF. A mechanized logic of computation
• Simplification by Cooperating Decision Procedures
• A Practical Decision Procedure for Arithmetic with Function Symbols
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item