{"entities":{"Q1595929":{"pageid":1606669,"ns":120,"title":"Item:Q1595929","lastrevid":47573989,"modified":"2026-01-02T03:02:47Z","type":"item","id":"Q1595929","labels":{"en":{"language":"en","value":"Structured theory development for a mechanized logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1565456"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1595929$79D31645-B5D2-489C-ACFB-6A5F8398B809","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"568b8e65da811d36dc59958601661a663384db18","datavalue":{"value":{"text":"Structured theory development for a mechanized logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1595929$9887A20B-0C22-47B4-9B6F-DA6C9D18AC93","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7ece6040257ffe084baa43fd58ec23026555ecfc","datavalue":{"value":"0971.03017","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1595929$A7635432-8FA0-467F-9E3B-4042DD2D0DC1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fd31f32b8ec35edb2553f5262f7bd46fbd33f2f5","datavalue":{"value":"10.1023/A:1026517200045","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1595929$559F4163-EAC9-4AFD-A20C-D55941A3F1D2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e6bbab2ea230ef82cf7d72bee404dd827d5aaeed","datavalue":{"value":{"entity-type":"item","numeric-id":230814,"id":"Q230814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1595929$BFC031EC-0612-42DE-946D-85AD7358D559","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b0d384413a2d1b8185eb46b74e5b2c74244e0aac","datavalue":{"value":{"entity-type":"item","numeric-id":928667,"id":"Q928667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1595929$ACA581BC-63A4-4ABB-A258-345D81DD2C8D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1595929$41909076-45C5-4901-B382-387D4DE64629","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a8d78bbdd3da8fc3032632626b45818e0358b86b","datavalue":{"value":{"time":"+2001-02-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1595929$B912A2B5-ED30-47BA-8D26-CCC05727FFD0","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"7b3ab7da85abc6ce66098956d3b5986153d2f199","datavalue":{"value":"Several aspects concerning the structuring mechanisms for the ACL2 (A Computational Logic for Applicative Common Lisp) theorem prover are presented in this paper. A brief overview of ACL2 is realized. Two notions of admissibility for recursive definitions are introduced. The notion of ACL2 history is introduced and this notion formalizes the result of a user's interaction with ACL2. The theorems of a chronology are consequences of its axioms.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1595929$732366BC-4009-4897-A0C0-B5548F5FF597","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1595929$6681F1A2-6E0C-43D6-95D9-72F9FA577EF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1595929$3D255652-AE89-431B-A89A-8C5CDBE75D39","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"90464406f400547f6395543cc35350695215ed83","datavalue":{"value":"1565456","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1595929$88EB45C7-9500-4FA0-9D02-138922F9F0CE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2e80a7123e4ea6d0418cb24d37b1837f13e3514","datavalue":{"value":"first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1595929$BDCF91F2-37A6-427F-8210-C6F161F07EE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q1595929$8CDACBF5-15FC-4650-96A8-057E87258D65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"24dd5926fa2c4f0ee181b086899e10f05b3e9148","datavalue":{"value":"ACL2","type":"string"},"datatype":"string"},"type":"statement","id":"Q1595929$81A186AB-58D5-4722-BDC2-DAC955C9104A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a2392b672efbd1bb0bba2c5ac67141a3f83c1afc","datavalue":{"value":"constraint","type":"string"},"datatype":"string"},"type":"statement","id":"Q1595929$FBE60B44-68A3-4812-8CBC-C00CCBFA35D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"55aee8f65ed799251e0440c5328251b805f6b23e","datavalue":{"value":"encapsulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1595929$DAF83BAE-8719-499A-8886-A20DAAC241DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"febb5b9d9c4c4fe28f149afcd5d966b304430791","datavalue":{"value":"functional instantiation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1595929$4A468176-CEE2-4326-AF22-7CA854063C88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe51228e17b836f3520db7bc0de40e5086eebee3","datavalue":{"value":"soundness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1595929$2A61529E-B17E-40E0-9110-F9F61B1AAF3D","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"9fb773d0cd3a039a126cfc91f47bdfc04e0ccc60","datavalue":{"value":{"entity-type":"item","numeric-id":1166490,"id":"Q1166490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1595929$CA3C0ED7-A274-415D-B705-7209C83E6383","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1595929$6AD0C7F2-6BC8-4CFC-BE1B-95AA7C5ABFCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a8f057223c758d6b8295ecbdef4842faac2ccb72","datavalue":{"value":{"entity-type":"item","numeric-id":19253,"id":"Q19253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1595929$32FB5AB1-87E7-4305-B3AE-BAAFB83254A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1595929$9314EB57-2D34-4815-ADB3-E7AA76BAFFF9","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1595929$F49A273E-FF7D-464E-9219-1EC9FEFF64A4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3c1e87e97bdeb5a915851b51cf265b3a989ece45","datavalue":{"value":"https://doi.org/10.1023/a:1026517200045","type":"string"},"datatype":"url"},"type":"statement","id":"Q1595929$94434735-D7E9-47A7-8605-1B2C833720ED","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"74d0d9f3e444ff1b2ef6b4ec50248d7e8dfda613","datavalue":{"value":"W1588366745","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1595929$CFA93E94-9CDC-4842-A685-0D653651083D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cf2c48c52bdc7c8427d6f3c28effe97624b0aac1","datavalue":{"value":{"entity-type":"item","numeric-id":2734953,"id":"Q2734953"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8a470994a72c1e2b2338b663916e715cc7553770","datavalue":{"value":{"amount":"+0.8392548561096191","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1595929$60BEFCAE-6EFA-467E-8DA5-5A6236CC7D96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2ab816ca20d777bf64b417cd94a39c25aff51b17","datavalue":{"value":{"entity-type":"item","numeric-id":4817211,"id":"Q4817211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"858855893a994c80d72922b21d6eaa15155487ff","datavalue":{"value":{"amount":"+0.8065289855003357","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1595929$782F2778-B4D5-45BE-B730-2D64DF853B24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b3b0efa447d2f0bb1d07cfcfcea727ec3cbe250","datavalue":{"value":{"entity-type":"item","numeric-id":2280212,"id":"Q2280212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"19e242e093942181c27b3c5ba31bffcb8bf5daac","datavalue":{"value":{"amount":"+0.7832528352737427","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1595929$7D147739-A18C-4450-98D0-3A6A8AE531F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3cda481b541398e1a99f4b5d3ef12a328b1ce13e","datavalue":{"value":{"entity-type":"item","numeric-id":6488518,"id":"Q6488518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5bb0d75283d225128a3658e3e4d65cca6c586e79","datavalue":{"value":{"amount":"+0.7762157917022705","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1595929$2B4CE143-A172-4270-A5FF-115139EEAF2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d9c7e2906cab0df39eaaaec6ded4334d15f17931","datavalue":{"value":{"entity-type":"item","numeric-id":4471942,"id":"Q4471942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cc3896766024f3b7227c3cd67cc618538bb15e6a","datavalue":{"value":{"amount":"+0.7683987617492676","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1595929$EAABF5B6-3A24-4E5F-9C74-E75970F3F5FC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1595929","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1595929"}}}}}