id: 580e7c719bdf4e09bdd9375e6a0e856d
parent_id: 19a3c030a55740e28660160b33a8988f
item_type: 1
item_id: c66c0433c6a14de9b9a40e5a7316e382
item_updated_time: 1696433711834
title_diff: "[]"
body_diff: "[{\"diffs\":[[0,\"ng: \"],[-1,\"Seventeen Provers Under the Hamme\"],[1,\"Automated Reasoning for Miza\"],[0,\"r\\\n\\\nW\"]],\"start1\":419,\"start2\":419,\"length1\":41,\"length2\":36},{\"diffs\":[[0,\"TH1+._\\\n\\\n\"],[1,\"## Automated Reasoning for Mizar\\\n### What is Mizar\\\nMizar is \\\"to a large extent a first-order system, enhanced with a number of extensions that make the formalization in Mizar more human-friendly\\\".\\\nExtensions include:\\\n\\\n - Mizar types: \\\"soft\\\" predicate-based type system, allowing for type hierarchies\\\n\\t - In essence, any term with a given type satisfies the predicates in the type hierarchy defined by the type\\\n - Structure types\\\n - Second-order constructs\\\n\\t - Axiom scheme of replacement, axiom scheme of comprehension\\\n\\t - MPTP can encode instances of such a scheme, but the scheme itself is inherently second-order, hence not encodable\\\n\\t - \"],[0,\"\\\n\\\n## Arc\"]],\"start1\":14629,\"start2\":14629,\"length1\":16,\"length2\":657}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-10-04T15:36:56.608Z
created_time: 2023-10-04T15:36:56.608Z
type_: 13