{"entities":{"Q679252":{"pageid":681101,"ns":120,"title":"Item:Q679252","lastrevid":63531804,"modified":"2026-04-11T13:48:07Z","type":"item","id":"Q679252","labels":{"en":{"language":"en","value":"Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1002306"}},"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":"Q679252$DD6EBA10-D192-4235-9D32-933F11416486","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bc7696865cf30c84b8f888ade2a540ba2aafabec","datavalue":{"value":{"text":"Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q679252$964A4115-8DB0-4ECE-942A-8C94DDE64B5A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dadee4c3861e8a208379513b606d52b609a5e0ff","datavalue":{"value":"0871.03004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q679252$281487BF-6214-40AF-B91A-2BAB60FC5241","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9eed5f2e6d9f96ae4d295491070309619fda6b17","datavalue":{"value":"10.1023/A:1005749401809","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q679252$77CB5892-AA31-417D-ACE8-955E13E9BDA8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"98a55778c503dc0554464020cdbb067d3e7b7378","datavalue":{"value":{"entity-type":"item","numeric-id":200696,"id":"Q200696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q679252$36E3BAA9-C2BE-4A95-B13B-022B2DB0C50E","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":"Q679252$6EC50939-7BE0-430B-9DBF-2D64C51B5EAF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6be3e37c641cde91cfa734d9536de0ec5c1b8bc6","datavalue":{"value":{"time":"+1997-09-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q679252$5EAFF2EF-E92E-45EC-983D-752CC1D60966","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"70dadbe96666f1c2e8be51f14a4a48a918245581","datavalue":{"value":"In this paper two algorithms are presented for eliminating and introducing quantifiers without Skolemization of the wffs, and the unification theorem for them is proved. Using these algorithms the author has implemented an automatic natural deduction proving system. The Andrews challenge problem as well as the halting problem are proved by this system.","type":"string"},"datatype":"string"},"type":"statement","id":"Q679252$1B8519C8-E0CE-472E-A5BA-802433C236EF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q679252$E94A5FAA-F83E-4EA4-BD0B-FD4EA3A83036","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q679252$D8420A0C-6E57-4551-B15B-1323745BF3C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"176e47af9f9e7cf4ebff07fc1f9e4f94a83134c1","datavalue":{"value":"03C10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q679252$F4EFC65A-A31C-4690-819A-CC87D443BA6A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9322df65593f1849fb213a498bca257319f4128d","datavalue":{"value":"1002306","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q679252$5A3686C1-6DF9-4583-8FD2-EF2BEA8B6328","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q679252$B700FECF-94AA-4D25-B666-30AA4CF4E445","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7e5d568140a653e809fe0aab6e5f93619204cfe","datavalue":{"value":"Gentzen system","type":"string"},"datatype":"string"},"type":"statement","id":"Q679252$9F796EED-FE64-4FF7-B70D-94FE107AB206","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"372cb15de3004a467e66d53d6552e691fb87a439","datavalue":{"value":"unification algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q679252$98465037-E820-4B13-B08D-FA4B19EF3CB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6d2d97828ccc83b19225a5cc30701cae23134926","datavalue":{"value":"automatic natural deduction proving system","type":"string"},"datatype":"string"},"type":"statement","id":"Q679252$5AFFA439-D12E-484C-8CB0-66F814612F33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8ee3910f9f817c7110e751420a2406186c243079","datavalue":{"value":"Andrews challenge problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q679252$A1AE4FE4-7AEB-418B-A493-C678E6B77C4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c9b38447a3ea959cbe95310edeeb21e7ef6903f8","datavalue":{"value":"halting problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q679252$7D87999A-6FB0-43C1-8EA1-AADB9077253A","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":"Q679252$853E558F-7699-4D56-B8C3-C06E606A8536","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7e54f4df77577ed046cbae6af65e9233cb2763f0","datavalue":{"value":{"entity-type":"item","numeric-id":18928,"id":"Q18928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q679252$60E0FFA8-5BE0-409F-87D5-FEABD4C3AF50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1aec27d540e360c78ddad230e6e300ced62bdec3","datavalue":{"value":{"entity-type":"item","numeric-id":18433,"id":"Q18433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q679252$28CC0AC8-FAD1-4084-85EF-2D9861DB6543","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":"Q679252$4C31AEC5-6296-4607-BDCA-4607F34BDE13","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"01b403c6e41bfb99d27cebec0d420c42f9e5bb62","datavalue":{"value":"https://doi.org/10.1023/a:1005749401809","type":"string"},"datatype":"url"},"type":"statement","id":"Q679252$DCF41443-6435-4390-8B2A-15DA51D6D894","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4163d099afca7f4594c9622c6e80bef832245289","datavalue":{"value":"W1499666987","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q679252$1DCFD4CD-9411-424E-9033-5B665E7E4D78","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"76fd7c463a84fbcbfc71cb42de2070b55b676079","datavalue":{"value":{"entity-type":"item","numeric-id":4610323,"id":"Q4610323"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a9a5c8f04cb72ce60862ce94b0970223c58378d4","datavalue":{"value":{"amount":"+0.826463520526886","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":"Q679252$19E200C6-11C2-4125-8E89-E78C0833D334","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d05bfdfcf8c95188bd6d35285d9394cf28891cd","datavalue":{"value":{"entity-type":"item","numeric-id":3780488,"id":"Q3780488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"87f353d53b869958cfb9c024e5cc6d2d9b9f1d1f","datavalue":{"value":{"amount":"+0.7589424252510071","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":"Q679252$5F20F4D7-29AC-4AFF-A6E5-86B12C4A6762","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a112d1013d75b0ddf62d8793fee33d050d77f8b1","datavalue":{"value":{"entity-type":"item","numeric-id":4681159,"id":"Q4681159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"21d6820f12df81cfb231331c4460a8efd1a54f37","datavalue":{"value":{"amount":"+0.7577619552612305","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":"Q679252$476F0C7A-A221-453C-8C2E-E81888108ECE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"64e3a16fe5cccad5236a53243e77de9015e09ae1","datavalue":{"value":{"entity-type":"item","numeric-id":792298,"id":"Q792298"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f107ced1517689de79480f50a99d5dbfa6787813","datavalue":{"value":{"amount":"+0.7558306455612183","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":"Q679252$52B977D7-BEE8-4675-83EA-DC25FCDDBCD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"295eacd5d3b86ddd32e0b401d6a1ad02be5bfe37","datavalue":{"value":{"entity-type":"item","numeric-id":808295,"id":"Q808295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e56e7d3090670b875e6bd111610ece881f59bd56","datavalue":{"value":{"amount":"+0.7419805526733398","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":"Q679252$D70C3D1E-8731-4177-BF2D-3805115383EB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Unification_algorithms_for_eliminating_and_introducing_quantifiers_in_natural_deduction_automated_theorem_proving"}}}}}