{"entities":{"Q6869946":{"pageid":20716267,"ns":120,"title":"Item:Q6869946","lastrevid":75237946,"modified":"2026-04-18T07:28:12Z","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"}]},"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"}}}}}