id: def16909303948ec87ccfabb1f54b97b
parent_id: bd5ca5ecdf1c41248c6b6118e0ae4cc8
item_type: 1
item_id: c66c0433c6a14de9b9a40e5a7316e382
item_updated_time: 1696517973719
title_diff: "[]"
body_diff: "[{\"diffs\":[[0,\"`.\\\n\\\n\"],[-1,\"\\\n### Proof reconstruction\"],[1,\"Can get more complicated when types are combined, like `A: ~finite & graph` (see paper).\\\n\\\n### Proof reconstruction\\\nYou could trust the ATP proof and not bother to reconstruct the proof in an ITP. Users of proof assistants generally frown upon that, however, and only trust a proof if it can be checked by the ITPs inference kernel. That requires some form of _proof reconstruction_, of which there are three main approaches:\\\n\\\n- Replay the ATP proof directly, inference by inference\\\n- Check the ATP proofs using a verified checker (for instance, one written in the proof assistant)\\\n- Translate the ATP proof to the proof assistant's source form.\\\n\\t- Translate can be very broad; Sledgehammer can use ATPs as basically a highly precise relevance filter, passing the premises used in the ATP proof to `metis`, a first-order prover that is extremely well integrated with Isabelle/HOL.\\\n\\t- \"],[0,\"\\\n\\\n##\"]],\"start1\":18054,\"start2\":18054,\"length1\":33,\"length2\":891}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-10-05T15:00:00.096Z
created_time: 2023-10-05T15:00:00.096Z
type_: 13