id: 40473d215d7340999075c429b822f599
parent_id: e3f3da79b37f418eb0fd8b9ad422bc0e
item_type: 1
item_id: c66c0433c6a14de9b9a40e5a7316e382
item_updated_time: 1695991546168
title_diff: "[]"
body_diff: "[{\"diffs\":[[0,\"ng: \"],[-1,\"Three years of experience with Sledgehammer\"],[1,\"Sort it out with monotonicity\"],[0,\"\\\n\\\nWi\"]],\"start1\":137,\"start2\":137,\"length1\":51,\"length2\":37},{\"diffs\":[[0,\"016)\\\n- [\"],[-1,\" \"],[1,\"X\"],[0,\"] Three \"]],\"start1\":1193,\"start2\":1193,\"length1\":17,\"length2\":17},{\"diffs\":[[0,\"seful:\\\n\\\n\"],[1,\"- [ ] Sort it out with monotonicity (K. Claessen, A. Lillieström, N. Smallbone, 2011)\"],[0,\"\\\n- [X] T\"]],\"start1\":1323,\"start2\":1323,\"length1\":16,\"length2\":101},{\"diffs\":[[0,\"004)\"],[-1,\"\\\n- [ ] Sort it out with monotonicity (K. Claessen, A. Lillieström, N. Smallbone, 2011)\"],[0,\"\\\n\\\nOt\"]],\"start1\":2113,\"start2\":2113,\"length1\":94,\"length2\":8},{\"diffs\":[[0,\" one-lin\"],[-1,\" \"],[0,\"e\"],[1,\" reconstruction (quite common now?); throw the proof away and let Metis find its own proof using the lemmas that took part in the ATP proof. In this case, Sledgehammer is basically a big relevance filter for Metis.\\\n\\\n### Proof minimisation\\\nATPs often return bigger axiom sets than strictly necessary; can be improved by running the ATPs on subsets of the returned axiom set until a minimal axiom set is found.\\\n\\\n### Miscellaneous\\\nSledgehammer \\\"now communicates with ATPs using full first-order logic instead of clause form\\\" - what does this mean?\\\n\\\n## Sort It Out with Monotonicity\\\nThe idea of monotonicity is fairly important in _Encoding..._, so reading this first seems prudent. It's also fairly short, and probably easy to get through.\\\n\\\n#### What is monotonicity\\\nMonotonicity is a property of sorts (~= types). The domain of a _monotone_ sort can always be extended by extra elements without affecting satisfiability. This allows us to group all monotone sorts together, reducing the need for typing information.\\\n\\\n\"],[0,\"\\\n\\\n## Arc\"]],\"start1\":8570,\"start2\":8570,\"length1\":18,\"length2\":1032}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-09-29T12:49:33.431Z
created_time: 2023-09-29T12:49:33.431Z
type_: 13