Reconstructing proofs at the assertion level

DOI10.1007/3-540-58156-1_53zbMath1433.68551OpenAlexW1480335431MaRDI QIDQ5210809

Xiaorong Huang

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:hbz:386-kluedo-2297

Mathematics Subject Classification ID

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

Related Items

ILF-SETHEO ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ Presenting machine-found proofs ⋮ Sledgehammer: Judgement Day ⋮ Finding good proofs for description logic entailments using recursive quality measures ⋮ Harpoon: mechanizing metatheory interactively

Uses Software

• Nuprl
• Automath
• LCF
• Omega-MKRP

Cites Work

• The translation of formal proofs into English
• Edinburgh LCF. A mechanized logic of computation
• Untersuchungen über das logische Schliessen. I
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item