{"entities":{"Q6869946":{"pageid":20716267,"ns":120,"title":"Item:Q6869946","lastrevid":84234122,"modified":"2026-05-14T00:22:38Z","type":"item","id":"Q6869946","labels":{"en":{"language":"en","value":"A stepwise refinement proof that SCL(FOL) simulates ground ordered resolution"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8149358"}},"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":"Q6869946$23BA5D33-8305-44A4-A066-CFA3C188D267","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dd55395702c66021d5bdb36363cc28928148e806","datavalue":{"value":{"text":"A stepwise refinement proof that SCL(FOL) simulates ground ordered resolution","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6869946$3A513DBC-F5E2-44B8-AE76-66072FAF2E05","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bd17a7fb9b9a9e46b9659ec223462c99070e5403","datavalue":{"value":"10.1007/978-3-031-99984-0_17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869946$BB5C8193-9B7D-42B6-947A-E6F5F6388F2F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fa7d05503577a5b9fd70ce583a8b9f4a6bc04b14","datavalue":{"value":{"entity-type":"item","numeric-id":831910,"id":"Q831910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869946$7E40F72B-BD8F-4BE1-9889-0AE36A0CEB33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"17c6d08c5d40a2588ec2b2e7f20fd42f41187444","datavalue":{"value":{"entity-type":"item","numeric-id":1687530,"id":"Q1687530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869946$B67D1200-E62A-4699-89D6-66ED145A9830","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e858e644a5f8f9e799cff3da307c11b687abc60c","datavalue":{"value":{"entity-type":"item","numeric-id":831914,"id":"Q831914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869946$26E210A9-F72A-492C-9980-A6796BD22CD1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"bd0535754d1571e407a6ce2636467dab5aaebc85","datavalue":{"value":{"time":"+2026-01-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6869946$6B7CC9FE-6A0C-4DEC-8088-E5A783CE3FDD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869946$06BA253E-5BEF-4FF0-B29C-003B482890F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869946$800A2915-2B12-40C0-8F70-472E2094F371","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869946$3A6203C5-317A-4B14-BC22-5299F99F3449","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6d577da3bca728f4a15cbf0f2e43f1d7cabea39d","datavalue":{"value":"8149358","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6869946$038C81A3-4D97-4575-9E9D-62F379A95D55","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":"Q6869946$08F3E75C-D331-4288-A34A-16F461B50046","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869946$D03E8BD0-9839-4DBA-B43E-6CF09D7729DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aa49441cb236b8b65abbf6ed9c73c7cae240e11d","datavalue":{"value":"(ground) first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869946$7E7F065F-4C65-4474-8FCA-BFA7A7327298","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"481b70e2eacf616ce4ff5d04385db4de7a56d954","datavalue":{"value":"SCL","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869946$C2A5D179-C686-4433-A83E-11F8036423C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddad87ca98e3caff019511d0ae415662d6845cb2","datavalue":{"value":"non-redundant clause learning","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869946$2398A5C8-3435-4651-B947-F1F167E8FBAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7e3cf9bca78e19102e6a3c7dfa3a53aed9896da","datavalue":{"value":"ordered resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q6869946$52BF4FFC-B16B-4648-83F5-52743FD36D5D","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":"Q6869946$E00A0D65-3C52-4F18-A628-A29FFF418C9B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aefe5e0f2b827afb25f0a8067d25c4a893f91ca","datavalue":{"value":{"entity-type":"item","numeric-id":4304492,"id":"Q4304492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869946$3046B206-0E15-48C1-9251-CCD8EFF3705F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"edad75aaaa58c4ce3df2557009b5af7431e58b1b","datavalue":{"value":{"entity-type":"item","numeric-id":1920207,"id":"Q1920207"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869946$41D1697D-93C8-45CB-8E22-5E5512DFE76A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84186d2e75fc83d00b617d151cea62695d8ba362","datavalue":{"value":{"entity-type":"item","numeric-id":6492734,"id":"Q6492734"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869946$2F39ECB4-A0E2-472A-9D5B-27CEEDBDDB97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6d72b96c91ebf8c923998f114a10233088e5f587","datavalue":{"value":{"entity-type":"item","numeric-id":2234101,"id":"Q2234101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869946$85C83D91-70A0-4C0A-85EF-26EBF5E51DBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab75901b0651ea9dcc948efb1ff1e44c7aa7ae8c","datavalue":{"value":{"entity-type":"item","numeric-id":6492736,"id":"Q6492736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869946$9A0B4C9D-4609-48EF-A6FD-CE87914282F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4342eaf993d8aed1454efafe9d939daad5b5ce67","datavalue":{"value":{"entity-type":"item","numeric-id":6860021,"id":"Q6860021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869946$A9CF16CC-A257-4F4C-A9F1-1B2B9D03F3CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d1db31f69f14e867729757963150857470e58a6","datavalue":{"value":{"entity-type":"item","numeric-id":2305416,"id":"Q2305416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869946$3D0D41E8-6B8B-4300-8BB0-4183144FFFCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1e0b4fc54e8c62a86959e50d4b1b27d9d9a092c","datavalue":{"value":{"entity-type":"item","numeric-id":5581665,"id":"Q5581665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869946$40CEDE6A-80FD-4D87-BF8B-64E3528D5ECC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4359d4aec7656095d8cff872a7ceb2994995e93a","datavalue":{"value":{"entity-type":"item","numeric-id":2104511,"id":"Q2104511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869946$31E0FD58-6980-4B85-A11C-B68EE4676992","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"333782dfe2a782886768e8c7561d4e8bfd035e1a","datavalue":{"value":{"entity-type":"item","numeric-id":2655327,"id":"Q2655327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869946$B4D92423-6BEB-46D7-82DF-847BE144D8B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"443687e1644d765aff7a815618637b8d7305da63","datavalue":{"value":{"entity-type":"item","numeric-id":5919011,"id":"Q5919011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6869946$1B83DD92-2329-443F-9BEA-CB90DA946E1D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A stepwise refinement proof that SCL(FOL) simulates ground ordered resolution","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_stepwise_refinement_proof_that_SCL(FOL)_simulates_ground_ordered_resolution"}}}}}