{"entities":{"Q6611963":{"pageid":14223120,"ns":120,"title":"Item:Q6611963","lastrevid":103626134,"modified":"2026-06-06T07:46:26Z","type":"item","id":"Q6611963","labels":{"en":{"language":"en","value":"Verifying a sequent calculus Prover for first-order logic with functions in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7919844"}},"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":"Q6611963$572DC337-30F9-417D-A1E6-9B639F5BD46A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bd7a12453a21c5331299c43b169ba9921c218e9c","datavalue":{"value":{"text":"Verifying a sequent calculus Prover for first-order logic with functions in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6611963$BF9269A4-B9BF-451F-B6F7-585EC7101219","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6b28ef1f69804175267e0c47b9aca79300dfa007","datavalue":{"value":{"entity-type":"item","numeric-id":2096469,"id":"Q2096469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$298495C4-BDF6-4021-972E-756DE671D739","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"64bef53befef37231db7bcfa82edd862395ab772","datavalue":{"value":{"entity-type":"item","numeric-id":6572547,"id":"Q6572547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$F5D17107-E654-44CE-A04A-984EA882C08E","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":"Q6611963$13178DDA-C973-4850-A558-C27D82D23C5A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"fa77625b6793398e9785907ea2f3653fa0fbf243","datavalue":{"value":{"time":"+2024-09-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6611963$F9DEE718-6E34-40F6-929C-A7DB5AA33AE5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6611963$1F1346FB-CDEF-455F-B928-1A74BDA582E4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3ebb3f569e57146d8353c06210e554961ffeee48","datavalue":{"value":"7919844","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6611963$BDE9F4DE-06DC-41C9-AFA2-61712C8EF920","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q6611963$AED9A2CE-B9AA-488A-A611-9E2420482308","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0791e5718a3ebc7d54d3973aabd3f04a763d17d8","datavalue":{"value":"SeCaV","type":"string"},"datatype":"string"},"type":"statement","id":"Q6611963$05DE6279-473D-41FE-ABE1-ADF797167F7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2e80a7123e4ea6d0418cb24d37b1837f13e3514","datavalue":{"value":"first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6611963$B014E414-89C3-44BC-A10B-57E56C7EAC4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"374e985ac2f37c53e9da15f7cd908117842a9c0d","datavalue":{"value":"Prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q6611963$3DC32B8E-FEF4-4E2F-8B4B-D7DA17FE78F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe51228e17b836f3520db7bc0de40e5086eebee3","datavalue":{"value":"soundness","type":"string"},"datatype":"string"},"type":"statement","id":"Q6611963$72B50F91-6553-45B4-B297-70EA0CF8C3AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4fc8534b3bb8a981c00a2744422055e258daa4c0","datavalue":{"value":"Completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q6611963$A63D783E-3035-4DD5-B8EE-FFC46D9229BB","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":"Q6611963$09A65DEF-736A-4906-9997-929FD983C527","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4738798d9702e646d9743f53f948745583da971","datavalue":{"value":{"entity-type":"item","numeric-id":2352487,"id":"Q2352487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$9831570D-3C22-4AFD-AD9C-949AC1C0AD1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"95f5e5a42b14858827b86e355a072cbbd1bdb099","datavalue":{"value":{"entity-type":"item","numeric-id":2894076,"id":"Q2894076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$7EE09D72-FF84-4C45-9708-0BD881BE56AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6f8c21e6d82f31fa2f7618306ddf28c9bb5b315","datavalue":{"value":{"entity-type":"item","numeric-id":2055874,"id":"Q2055874"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$CACAA4E3-0807-4616-AB7B-21A949EF1F30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0202cb9cafa0358b07911808cfce41ae5240485b","datavalue":{"value":{"entity-type":"item","numeric-id":3192180,"id":"Q3192180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$041F33E9-1A28-490B-ADBC-12CA116DD91B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"399034269be6bba8be1aee8f83a7563dc96523db","datavalue":{"value":{"entity-type":"item","numeric-id":2849493,"id":"Q2849493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$02DF5BD8-F2FB-457D-82E5-7EFCB66F2093","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"00c2d672d21d4d5af646f31d9599e67b8b6b153b","datavalue":{"value":{"entity-type":"item","numeric-id":1663234,"id":"Q1663234"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$28CAA983-A6D4-4ACA-8C55-E5C49B4FB52A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ac39b9a75827004294f51289a3c3e79253c87a2","datavalue":{"value":{"entity-type":"item","numeric-id":2362498,"id":"Q2362498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$C9D0FB9D-EFB4-4E44-A777-8FF39E3CD0E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2da17dad5fd4641d64373f0fc66dbe3dd437187","datavalue":{"value":{"entity-type":"item","numeric-id":2829254,"id":"Q2829254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$C2D49081-AEEB-4FBB-A080-AB5552A835F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"171f2f23484cc563361b9a949250d7cf0cf0889e","datavalue":{"value":{"entity-type":"item","numeric-id":2479551,"id":"Q2479551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$DD8D349F-4F77-441F-A6FD-18CCFB77EA18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c4d9dbe5c8efa8434d8c6872c1bda9d6b35f241","datavalue":{"value":{"entity-type":"item","numeric-id":6572548,"id":"Q6572548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$D294B2A6-35CD-49F8-BD8F-A3E2EE61C4A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ade297681f99165268de8e931d390854dd4d3634","datavalue":{"value":{"entity-type":"item","numeric-id":2148773,"id":"Q2148773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$5116BD17-1626-4FC5-8EC1-3D223C66D62C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc3b3847af2322ff8f44d7e840cb1220d0277bfb","datavalue":{"value":{"entity-type":"item","numeric-id":5145439,"id":"Q5145439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$D8DA5F56-37FA-4E3F-BB96-3865A578579F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a1a0dcbfc561e1e5ffac774e9501a5c3c966797","datavalue":{"value":{"entity-type":"item","numeric-id":1722645,"id":"Q1722645"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$E1EC2C5E-DF3C-4E82-B9E8-ECCA8AC11217","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1951f16d4fe8a611f755a4887c35002e0149e28","datavalue":{"value":{"entity-type":"item","numeric-id":5919480,"id":"Q5919480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$D09670AB-F7FC-44FC-B4C3-5D189453B328","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"839fe9e80ad88458f41a8a24be5284fc203e2e80","datavalue":{"value":{"entity-type":"item","numeric-id":606999,"id":"Q606999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$37B9A5AF-97AF-496D-A2DE-0BA27D4C25AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b659b1f6009ab3df1cf8432adfeb1aaf4fe4f69d","datavalue":{"value":{"entity-type":"item","numeric-id":6060676,"id":"Q6060676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$6F411DBF-94D9-4701-809A-52760E938491","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dacd4f5ff8afe5c539d487d81ad8e6b7f661bae9","datavalue":{"value":{"entity-type":"item","numeric-id":4539651,"id":"Q4539651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$EE6C35A2-B4EE-4C04-BBB9-C08EC19CCB3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0924a86f652e00311e8961b2cdeee4e5aaf93ece","datavalue":{"value":{"entity-type":"item","numeric-id":1577335,"id":"Q1577335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$F9880B99-8A99-41C1-AE5E-E55CA79F1115","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58b883d872eefbd5f8daf82a38b9e66e81e1a15c","datavalue":{"value":{"entity-type":"item","numeric-id":5477663,"id":"Q5477663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$CF181A8F-5E53-4CCD-987C-E76598324C92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6247542da97c1bd60e1293202198b0e15650e479","datavalue":{"value":{"entity-type":"item","numeric-id":5916290,"id":"Q5916290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$2880B297-25E2-4A71-BD02-B8FB81E7113B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"38602d2b7fd482d2c85a2b53c450a23a2740fb43","datavalue":{"value":{"entity-type":"item","numeric-id":1663242,"id":"Q1663242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$087FA3C4-49B1-4651-B3A0-CD339F34313D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f769fe6ef8dd71200eafe07970c69907f40fbcb","datavalue":{"value":{"entity-type":"item","numeric-id":5179007,"id":"Q5179007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$80B1BF91-299E-4B88-92D1-96A6695A6BA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e386a86950f465930ae0749e91e9486062cb69bc","datavalue":{"value":{"entity-type":"item","numeric-id":4647860,"id":"Q4647860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$385C2ED5-E66D-409C-8BDB-55872EF4F215","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f82f0f40ab66cf033c5a229880b34de6b2284f9c","datavalue":{"value":{"entity-type":"item","numeric-id":1694574,"id":"Q1694574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$99F25B7C-D37F-48FF-BB9B-9A2D7100437A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b8eff4208337684da1d52cff1a28a6831c34fa8c","datavalue":{"value":"10.1007/S10817-024-09697-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6611963$E8BF5675-DA71-44EE-87AB-2FBE78B29DD5","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6611963$018C71D5-8ABB-4091-A3E0-00DD4F9DAFDF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Verifying a sequent calculus Prover for first-order logic with functions in Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Verifying_a_sequent_calculus_Prover_for_first-order_logic_with_functions_in_Isabelle/HOL"}}}}}