id: 2c990b8dc04a4c64bca9de95766f028e
parent_id: 6e683096df8e4191aa699a5a5ef5b20a
item_type: 1
item_id: c66c0433c6a14de9b9a40e5a7316e382
item_updated_time: 1696430275631
title_diff: "[]"
body_diff: "[{\"diffs\":[[0,\"hism in \"],[1,\"provers seemed not to be beneficial, nor was native support for Booleans, if-then-else and let.\\\n\\\nTF0 and TH0- performed the best for various provers (number of problems solved). Support for higher-order logic was occasionally useful; among 3321 total proved goals, 146 were only provable with higher-order formats (given the constraints of the provers).\\\n\\\n### Translation\\\nDifferent translations of polymorphic problems to monomorphic or untyped problems were also surveyed. In general, native support for polymorphism (TF1) was worse than translating to untyped FOF using the monotonicity-exploiting translations given in _Encoding..._. Note that this encodes the polymorphic logic in FOF, and is therefore complete. Although finite monomorphisation is incomplete, for most provers monomorphising the problem (TF1 -> TF0, or TF1 -> mono -> FOF using e.g. ~g??) was even more successful.\\\n\\\n_Finally, we notice that for all provers that support both TF0 and TF1, the monomorphized TF0 results are better than the TF1 results, and similarly for TX0 vs. TX1, for TH0− vs. TH1−, and for TH0+ vs. TH1+._\\\n\\\n\"],[0,\"\\\n\\\n## Arc\"]],\"start1\":13627,\"start2\":13627,\"length1\":16,\"length2\":1113}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-10-04T14:46:56.574Z
created_time: 2023-10-04T14:46:56.574Z
type_: 13