id: e3f3da79b37f418eb0fd8b9ad422bc0e
parent_id: 9d13fd40726349ce9550c6bc84b8041f
item_type: 1
item_id: c66c0433c6a14de9b9a40e5a7316e382
item_updated_time: 1695989851818
title_diff: "[]"
body_diff: "[{\"diffs\":[[0,\"clause\\\n\\\n\"],[1,\"Turns out: Sledgehammer sucked on higher-order problems. Makes sense, as it translated away higher-order elements and expected first-order provers to now deal with the significantly unwieldier first-order versions of the original problem.\\\n\\\nSimilarly, largely arithmetic problems posed difficulties as the provers were not well suited to them.\\\n\\\n### Relevance filtering\\\nRelevance filtering is tricky; the unsound translations that Sledgehammer used [this has changed; see Encoding mono... for a bit on monotonic types and their enabling of a sound translation] caused issues if the lemma set contained inconsistencies, which was only avoided because \\\"Sledgehammer['s relevance filter] generally selects too few lemmas to produce an inconsistent axiom set\\\".\\\n\\\n### Proof reconstruction\\\nIdeal: use the ATP proof and 'replay' it in Isabelle. Turns out, very difficult (ATPs often do not supply enough information).\\\nSolution: integrate one ATP which is specifically suited to this (Metis) with Isabelle, then use the axioms that the ATPs used in each proof step and pass them to Metis.\\\nInteresting alternative: one-lin e\\\n\\\n\"],[0,\"## Archi\"]],\"start1\":7475,\"start2\":7475,\"length1\":16,\"length2\":1130}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-09-29T12:17:34.803Z
created_time: 2023-09-29T12:17:34.803Z
type_: 13