id: 1bb07f5ee0ba457bb4153641a5df43c4
parent_id: 6f99949269534100ba54dcb9f6e5dcb2
item_type: 1
item_id: c66c0433c6a14de9b9a40e5a7316e382
item_updated_time: 1696514810575
title_diff: "[]"
body_diff: "[{\"diffs\":[[0,\"ethods\\\n\\\n\"],[1,\"### Premise selection\\\nSelecting relevant premises from a large library to pass to ATPs in order to prove a conjecture. Necessary because automated provers cannot really work well with a problem that has more than a few hundred premises. Has been challenging until \\\"recently\\\" (in 2016). Methods can be divvied up into non-learning approaches (based on heuristics), learning approaches (look at previous proofs) and combinations thereof.\\\n\\\nNon-learning methods: MePo (Meng and Paulson), selects facts based on commonality of symbols with the goal; SInE; etc (see paper)\\\nLearning methods: Naive Bayes, k-Nearest Neighbors, ... usually work on features extracted from facts and the goal to classify a fact as relevant for the given goal.\\\n\\\n### Translation\\\n\\\n### Proof reconstruction\"],[0,\"\\\n\\\n## Arc\"]],\"start1\":15656,\"start2\":15656,\"length1\":16,\"length2\":791}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-10-05T14:10:00.077Z
created_time: 2023-10-05T14:10:00.077Z
type_: 13