{"entities":{"Q1202066":{"pageid":1212815,"ns":120,"title":"Item:Q1202066","lastrevid":69875208,"modified":"2026-04-13T10:55:52Z","type":"item","id":"Q1202066","labels":{"en":{"language":"en","value":"Instantiation theory. On the foundations of automated deduction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 108164"}},"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":"Q1202066$8A7DF516-F2A6-4B57-B628-0DF887AC2D80","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5de2bccb1d21a3410b1f3536a94241c88b42a11c","datavalue":{"value":{"text":"Instantiation theory. On the foundations of automated deduction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1202066$A3144B3D-8602-418B-A156-CB078C202A18","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"163a28ee46f9e0806dee1da76d118b0933f5ac75","datavalue":{"value":"0785.68084","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1202066$7B3971A8-AEFD-4737-9601-D1AD030AD917","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"40be498166b3650078319ac29490b19067ad88d7","datavalue":{"value":{"entity-type":"item","numeric-id":333828,"id":"Q333828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1202066$4F00C281-2B9B-42D0-A331-216612557762","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1202066$BF917D18-3615-4F0D-BD90-9E96F2DD0F46","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4f64992dbeef321276c91b04bb85fa175c4114d8","datavalue":{"value":{"time":"+1993-01-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1202066$9374CAFE-237A-4A8C-A455-8E20F6B26125","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8fc7d1b95518b6d07d9b88ccec9d3d299acb875c","datavalue":{"value":"Instantiation, or the theory of variable substitution in terms, is studied here in an abstract setting. In order to make the theory as general and clean as possible, the basic concepts are introduced axiomatically, so that, rather than working upon any particular formalism, such as the terms of first-order predicate logic or lambda- calculus, all such term systems are examples. The climax of the text is a unification algorithm which is proven to be sound and, under appropriate conditions, complete; the complexity of the algorithm is also discussed. Other topics along the way include further properties that an instantiation system might enjoy, such as various degrees of type strictness and well-foundedness of terms, and quotient system, subsystems, and homomorphisms.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1202066$13015015-F560-4D0B-946A-D51B2D5171D7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1202066$58067FF0-75C0-4846-9986-26BB3BD27217","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"02303c61036060136df3f7b7e22c52163746633f","datavalue":{"value":"68Q99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1202066$413F13EF-468D-49AF-9E93-BF294665285D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1202066$EFD0D2FF-AA51-41F3-A563-AAEC23BD621E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"24aafcf24a21bd70cd3b62d3f5f72a6d0d82d816","datavalue":{"value":"68-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1202066$15DE0786-D967-4959-856F-F3241CCD9420","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e5272626df0be283f0c101cf98427ee1d6e88632","datavalue":{"value":"108164","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1202066$715D6D78-F1D7-4D38-82D6-85B4CB75DDF9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"33ecf041eedbe3fee8d29905fed91e77f22410fe","datavalue":{"value":"instantiation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1202066$221FC214-C84C-4048-BF66-313F524AAD4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3151651b96ed53c831f9445228069b640ffe335d","datavalue":{"value":"variable substitution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1202066$0F6AEA96-D53B-4DB9-8988-F09ED25C894A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4c5fb064a6e2a7ef2a613f518055d83bfe4e8a16","datavalue":{"value":"term systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1202066$21C7A799-1EF8-4633-887D-E81BCD079106","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3922eb0b8235fb2b824bcb3eaa0c8d395dbd512","datavalue":{"value":"unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1202066$D8B405BD-A83F-4458-ADC0-04AECC8D9835","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c5f8382ba04f9f05f645b4d0e4b9ea28f0619583","datavalue":{"value":"complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q1202066$FE93D73B-D4A4-465D-91A2-9736ED7F3EC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f78ff9a60b74189b2daec43f91e02e6e79fb14f9","datavalue":{"value":"well-foundedness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1202066$9369B8C9-FDA3-4FBC-BDC9-077BFE378ABB","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"7145106527c76ee3f2b876b4b260f13e7c40b44e","datavalue":{"value":{"entity-type":"item","numeric-id":408536,"id":"Q408536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1202066$14DA79CE-CAD4-423D-A01D-8CDCB6CC95F1","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b799da0cc0efb29a46dd283874e64386ca0e87dd","datavalue":{"value":{"entity-type":"item","numeric-id":21136,"id":"Q21136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1202066$87DDCAF7-75BD-43FE-BC07-9128ADC6EEB8","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":"Q1202066$15E918B3-F203-4023-A1D5-3F3FD61A241C","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":"Q1202066$80B37167-E5B0-43C4-B065-7F3A3D7374FD","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7c30078b1e62988cdde21fbe820decca7b08bad5","datavalue":{"value":"10.1007/BFB0031932","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1202066$2EDC8F15-DFB7-47DB-AE4A-67D55BFAE078","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2e4812f2fbf9b71399cd19e665d9364005ce30c2","datavalue":{"value":{"entity-type":"item","numeric-id":2751360,"id":"Q2751360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9b98e826a2e422056b275c9a1348656f8189f288","datavalue":{"value":{"amount":"+0.8288191556930542","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":"Q1202066$0DA3644C-2656-4FC1-BB68-0E5C8051D8F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8c7a85de369a018f61660f9b5d7e31a14e6ea8af","datavalue":{"value":{"entity-type":"item","numeric-id":3338215,"id":"Q3338215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"082ad9227bfe1e581e7d8218451aaed8d5e0c3b7","datavalue":{"value":{"amount":"+0.7706879377365112","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":"Q1202066$FE460410-4204-4064-B7EC-D430C3FB5B0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"be685d2cdc300dc0bdd4275522c6ab8f027d8ffe","datavalue":{"value":{"entity-type":"item","numeric-id":6169562,"id":"Q6169562"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9fa51f8089284b54bc8c36a3fd9893e6a170ee1c","datavalue":{"value":{"amount":"+0.7652151584625244","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":"Q1202066$76A6F5EA-B922-4AC8-8C21-06156AC806A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"01584f802a6f3e5e9a938324da32d68d107a4db9","datavalue":{"value":{"entity-type":"item","numeric-id":6169563,"id":"Q6169563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"661d010b4578aac9c9a1d7d31b5fdad37ce794d9","datavalue":{"value":{"amount":"+0.755620539188385","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":"Q1202066$A9F15B14-0E71-4188-BFE8-FAA962C94E2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bbb483c2684f4627d50245224e740d066f55a422","datavalue":{"value":{"entity-type":"item","numeric-id":3326880,"id":"Q3326880"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b4d79912723fd938bf31dcaba51cbdc452d060fe","datavalue":{"value":{"amount":"+0.751013994216919","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":"Q1202066$C3966D70-43F6-4BFC-BA67-015D08AFE1B2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Instantiation theory. On the foundations of automated deduction","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Instantiation_theory._On_the_foundations_of_automated_deduction"}}}}}