{"entities":{"Q2785674":{"pageid":2796412,"ns":120,"title":"Item:Q2785674","lastrevid":42012413,"modified":"2025-05-22T10:52:48Z","type":"item","id":"Q2785674","labels":{"en":{"language":"en","value":"Adding metatheoretic facilities to first-order theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 981819"}},"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":"Q2785674$5E665F87-320A-4FA4-9201-B7D10D6AA33E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5c9331bf0d2d365ba7f4df371618200378940d31","datavalue":{"value":{"text":"Adding metatheoretic facilities to first-order theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2785674$B01C6CF0-FB30-424F-A1A2-861B22042D02","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1c14ee20248510542907298bc2a1850c0472fb67","datavalue":{"value":"0868.03006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785674$99829F89-35D7-467A-916C-E2199216DA72","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ddc7b5b12b893092752e25f19fff9284b5a1df19","datavalue":{"value":{"entity-type":"item","numeric-id":1289099,"id":"Q1289099"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2785674$31D07C8D-CD60-4151-998F-74830C291FA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"69ad79c07c2956f1777e7c914202daf6884a50fe","datavalue":{"value":{"entity-type":"item","numeric-id":1332774,"id":"Q1332774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2785674$B77D8CEC-373A-4655-8306-EDE425740436","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b34f93578f34bf813eb265da2a0d58fb3d8dd5ea","datavalue":{"value":{"time":"+1997-08-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2785674$0C0BBD39-3289-494F-8607-29300ABEFE0E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"baf16c54ea3f27ff387b5757ba762c974013c7c3","datavalue":{"value":"https://semanticscholar.org/paper/75fd8190fa88eae3e5641ea7945e9659281303c2","type":"string"},"datatype":"url"},"type":"statement","id":"Q2785674$2F71C2E6-4754-4216-B778-79C76D56F4C4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785674$EF7B92AE-6076-443D-82A8-78F39652282A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785674$13FEEF1B-64B0-44DE-A4EC-A3AEB4E386AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d971f250f4b60bd91da7e9350568180af141e6af","datavalue":{"value":"03F03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785674$BF99D0AC-1E0F-42E3-AAAB-9BD293D1C015","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8c9cb6bf0b760187677a0a41368d47888e882510","datavalue":{"value":"981819","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785674$F8A199F6-F92D-4E22-BCE8-0B71C42153FA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3fd3e9ac85afddfac937c2bfadba05c5617f051","datavalue":{"value":"metavariables","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785674$8DA9CA17-C2A0-4787-9B31-51EA9DC55ED4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c2e05b6ddf912b5d08f772d0b458230312ddca6","datavalue":{"value":"quantifiers over formulae","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785674$934AC20E-9E8B-4770-8592-BEEA5245B3F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66a730f7536540ede475cba133b4e8ccce2cbb84","datavalue":{"value":"metatheory of generic proof systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785674$8B30EF6B-CFBC-4141-902D-E8EE14CDC771","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c78dae17f4c8390e58619a9d0e199fbb57e668af","datavalue":{"value":"weak extensions of first-order theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785674$8B8DD439-1EDB-45E6-8820-49A19231F216","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2785674$0B85ECC2-5AA5-40B1-BE47-2DC2D7999EF5","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":"Q2785674$8820C626-6D21-4349-B798-3420E7392EF1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f548d5eea4d213f7babae41c78ad09ca54ec7266","datavalue":{"value":"W2009919631","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785674$4A10F420-82BA-4091-971E-F4843CDFF112","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1dce1093d2f0a82f42839112213efd3f607dd656","datavalue":{"value":"10.1093/LOGCOM/6.6.835","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2785674$60556144-74A1-466B-94E8-539024D32480","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b7dc9418057f06a53b63781288396607ce78fe8","datavalue":{"value":{"entity-type":"item","numeric-id":4609965,"id":"Q4609965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2ced1cf1b71758d2b2bf8dbe946b0571785fad69","datavalue":{"value":{"amount":"+0.89030635","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2785674$088B33CF-E09F-4057-A945-BDBB54783931","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b2cf147eeab55487ae70a171c0208ad96b9ffa6f","datavalue":{"value":{"entity-type":"item","numeric-id":4340931,"id":"Q4340931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a6dedc8b3cdf31f53c46d0835c706f2566351013","datavalue":{"value":{"amount":"+0.8757272","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2785674$053D71C8-3A57-44F9-AEC6-6C6B27DF2FC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5dcb359b506a22c50bf7da6e8cd15766af11bd94","datavalue":{"value":{"entity-type":"item","numeric-id":4264727,"id":"Q4264727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9b98d5fd72a6048808ab1e4fb3f5c6ae0e5620c3","datavalue":{"value":{"amount":"+0.85890234","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2785674$D11BDB34-53C7-40DC-B561-DE511E1685ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"77ca390a037376bf0ee9810968554a6a01295767","datavalue":{"value":{"entity-type":"item","numeric-id":2892744,"id":"Q2892744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"446aa2c44b2f3f1f956486c9eb9e220e677920f5","datavalue":{"value":{"amount":"+0.85872406","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2785674$6A0D006E-76F3-4C20-A3EF-D2A0AC03BCE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"26d66e25d9de907b4c6db85700c3db748f95291f","datavalue":{"value":{"entity-type":"item","numeric-id":4208528,"id":"Q4208528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ba97baad32e40c4302f44373a070ba1374e5cc71","datavalue":{"value":{"amount":"+0.8579013","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2785674$75EAFABB-35B9-481F-9B82-698E31A5CEB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c5f74c2db6562d7bf942f3c79813489801a00d2b","datavalue":{"value":{"entity-type":"item","numeric-id":4304145,"id":"Q4304145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ba97baad32e40c4302f44373a070ba1374e5cc71","datavalue":{"value":{"amount":"+0.8579013","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2785674$16BA49E6-E601-4A87-AE18-E9479CEBF3E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4a5467214381d9eb97275e6ca78397919ead761","datavalue":{"value":{"entity-type":"item","numeric-id":5308093,"id":"Q5308093"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"32d9edf5bf9555a6e8368f7f5017794f125b453d","datavalue":{"value":{"amount":"+0.85671675","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2785674$2FC0DE38-508C-48E4-BAFA-069C532C5A2E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"40f594dc71eb8d0d9e416ce5ebbf0cbc7e358712","datavalue":{"value":{"entity-type":"item","numeric-id":2987751,"id":"Q2987751"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d438aaeac14f4185257e0e4b01ffb739aebff3b2","datavalue":{"value":{"amount":"+0.85233593","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2785674$06CB10CC-AEEC-4B48-B9E1-983CC3EE9E5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1841c0107b8bdc2b59e43c2e2095aaf7f436a891","datavalue":{"value":{"entity-type":"item","numeric-id":4305337,"id":"Q4305337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d2f95fa01c8608f00edf1398a9a7550aaab065f","datavalue":{"value":{"amount":"+0.8412298","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2785674$470AD01F-F40A-46CC-9FE9-285FF0E46B34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"350bbbcc96b3ac8c2c61b1f1bec9ed4cc54fd1e2","datavalue":{"value":{"entity-type":"item","numeric-id":2151399,"id":"Q2151399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5e0b9057860b18e36f2711a2b30162b18e00ce22","datavalue":{"value":{"amount":"+0.84095377","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2785674$77433689-183C-4883-BB16-FE8A38AE2FDE","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4e284497c1d95ed03031b32369f55bf404c9e002","datavalue":{"value":{"entity-type":"item","numeric-id":6768690,"id":"Q6768690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2785674$DE731626-6D5F-4F3B-8107-6E5D5036F51F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"0227d757f21f944415197768f8c9f3fcfbae53ca","datavalue":{"value":"Generic proof systems (like the Isabelle logical framework) provide some limited but useful metatheoretic facilities for declared logics; in particular, users can prove simple derived rules and also `solve' formulae that contain metavariables --- a technique useful for, e.g., program synthesis. The authors explore these two kinds of metatheoretic extensibility, and their applications. Their contribution is to show that rather than using a system like Isabelle, these kinds of extensibility can be directly added to an arbitrary first-order theory by conservatively extending it with quantifiers over formulae, that is, without recourse to an independent metatheory. This can be seen as a proof-theoretic investigation into aspects of the metatheory of various generic proof systems and how they can be simulated in weak extensions of first-order theories.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2785674$CF01938D-9DC5-4916-B447-A6843F636B77","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"ba8472b3da3fbe356de4dc8ca93e3dfd034c762e","datavalue":{"value":{"entity-type":"item","numeric-id":1332774,"id":"Q1332774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2785674$72113301-194B-4DB1-80D4-028A63B3B58A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2785674","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2785674"}}}}}