A metatheory of a mechanized object theory

DOI10.1016/0004-3702(95)00002-XzbMath1506.68178MaRDI QIDQ2676562

Paolo Traverso, Fausto Giunchiglia

Publication date: 27 September 2022

Published in: Artificial Intelligence (Search for Journal in Brave)

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Nuprl
• NQTHM
• LCF
• GETFOL

Cites Work

• A higher-order implementation of rewriting
• Prolegomena to a theory of mechanized formal reasoning
• Implementing tactics and tacticals in a higher-order logic programming language
• Multilanguage hierarchical logics, or: How we can do without modal logics
• Program tactics and logic tactics
• Model theory
• Edinburgh LCF. A mechanized logic of computation
• The foundation of a generic theorem prover
• Transfinite recursive progressions of axiomatic theories
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A metatheory of a mechanized object theory