{"entities":{"Q2726307":{"pageid":2737046,"ns":120,"title":"Item:Q2726307","lastrevid":79331018,"modified":"2026-05-06T13:40:17Z","type":"item","id":"Q2726307","labels":{"en":{"language":"en","value":"Tactic-based inductive theorem prover for data types with partial operations (Diss., Univ. Kaiserslautern, 1999)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1620775"}},"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":"Q2726307$0795CD2D-2C2E-4228-972D-002A10799684","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"81a3bdd12c828f843466f987f4e2ee5a61facf66","datavalue":{"value":"1037.68130","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2726307$D3FE8875-350D-474F-AD0E-63C0FFECC6CD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e7b7e20ab12ae2e121ebb631a7ac80de75fb7578","datavalue":{"value":{"entity-type":"item","numeric-id":2726306,"id":"Q2726306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2726307$CAB51C97-37B6-4675-BBE1-3BC521FE942D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"cb916ad91e9e27f9d11a7b9fee5e1117f9d898f2","datavalue":{"value":{"time":"+2001-07-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2726307$ED846260-9F55-4631-9BC4-83213BF96DF6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2726307$02F6F148-5E57-48A8-A1A8-A67B5FCAE7EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"73dccdfb072fb026a86af92d74fe625efeb2b023","datavalue":{"value":"68T35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2726307$56EB8171-A535-424A-A120-C8403803A5D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2726307$478F3AA7-35F6-42EE-B385-67DF972BD51F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e4380b05c700066c97bdcb46a218f0ac5557eee1","datavalue":{"value":"1620775","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2726307$4D3164C5-95E5-4FCE-95CA-12519682E0B4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fa6792ab787021778f5f20cba1d78917f3fc46dd","datavalue":{"value":"inductive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2726307$C6528D6E-6A73-4187-9465-A9F901711E0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6135ceafed3292f6b66e098192375f7d5b754046","datavalue":{"value":"inference rules","type":"string"},"datatype":"string"},"type":"statement","id":"Q2726307$FDAE5FB7-F415-4085-AC38-5E136262C85A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5e20ddaaa2513d952add876706745abc0cb4869e","datavalue":{"value":"proof control","type":"string"},"datatype":"string"},"type":"statement","id":"Q2726307$E3713509-623F-458D-B058-03F47C12E202","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ea032f14678abd54b0d55af14fe6fe1fdae52549","datavalue":{"value":"correctness of programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q2726307$6E231BF3-9DC8-439A-8526-DD70A29F8EBF","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6301cd18e3d0fd18796b3580abcdfb3469e82581","datavalue":{"value":{"entity-type":"item","numeric-id":38037,"id":"Q38037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2726307$207AC456-2CBE-4712-AF05-807E83CEE2A1","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":"Q2726307$CF6B13B8-2E5A-4CDD-A440-90506A582DE0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2e1170f1d08e84244fe633f8af9ac300a5dafdf4","datavalue":{"value":{"text":"Tactic-based inductive theorem prover for data types with partial operations (Diss., Univ. Kaiserslautern, 1999)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2726307$F226E391-A719-4F8A-9C27-166780D39AC2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ab20887f4e52f45c9e6920611057611555a8c68e","datavalue":{"value":{"entity-type":"item","numeric-id":6768709,"id":"Q6768709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2726307$1DEB45FE-575B-4412-8A6F-DBF248AA087E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"8307aaaaffbbcd9ce715422c4451e8aa02f2a4e3","datavalue":{"value":"The overall subject of this dissertation is how to bild a system that can prove corecteness properties of the programs in a functional programming language obtained as rewrite systems from conditional equations for abstract data types. The problems to solve are: fixing an expressive specification language, the choise of an adequate semantics, presenting a proof calculus consisting of inference rules, implementing a prover based on tactics, which the user can call interactively and providing a graphical user interface to support interactive proof attempts. In the first chapter, the author presents a formal framework for inductive theorem proving, including the specification language and inferences rules for representenging proof constructions. In the second chapter inductive theorem prover \\textit{QuodLibet } is introduced, including command language, the proof control language QML, QML routines and inductive proof strategies. In Appendices A, B, C, D and E are presented the proofs, the syntax and the inferences rules for \\textit{QuodLibet } and also syntax of QML and examples of proof constructions.NEWLINENEWLINEThe thesis can serve as instructional material for a course on theorem proving or AI at graduate level.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2726307$1BAFF0A0-99D2-40C3-A2E1-9FEC9EABF02D","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"850715937341d072522c2b6dfe4fd00f3d07e86f","datavalue":{"value":{"entity-type":"item","numeric-id":689296,"id":"Q689296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2726307$422C9041-0238-45C2-B316-380EB95024F8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eef1ed3065968672c17b7fba9f35c06dd0f65599","datavalue":{"value":{"entity-type":"item","numeric-id":2726294,"id":"Q2726294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"880ad879ef349c125d9596b40368047bbc30aa38","datavalue":{"value":{"amount":"+0.9078198075294496","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":"Q2726307$4503159D-2B54-4F14-9FCB-A03B2F288C63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1b18f1bcee5a559e76e86ee84dd5601244af54f6","datavalue":{"value":{"entity-type":"item","numeric-id":909488,"id":"Q909488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d2c605401f0421982f50d0e5f4e29f8243284183","datavalue":{"value":{"amount":"+0.7523096799850464","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":"Q2726307$25641433-7040-4B22-BFAB-187F66A22DD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b9c458cbc19644ec29358a69715d94a62d55eea","datavalue":{"value":{"entity-type":"item","numeric-id":4594217,"id":"Q4594217"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5e357707febe94fdbbfc0f3a2158c2cac1ec00fd","datavalue":{"value":{"amount":"+0.749514102935791","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":"Q2726307$4FDF2866-A114-4240-B7C2-0E9CAEED7188","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d8aa88f960b08160c56495dd31aafe873551353","datavalue":{"value":{"entity-type":"item","numeric-id":3732983,"id":"Q3732983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bf30b76f4f97a2d6f25475fffcdae1df10b2842d","datavalue":{"value":{"amount":"+0.7324222922325134","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":"Q2726307$A0FEC29A-6BDE-4EA2-B119-A293DDFEDFC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3cda481b541398e1a99f4b5d3ef12a328b1ce13e","datavalue":{"value":{"entity-type":"item","numeric-id":6488518,"id":"Q6488518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"efd7120d0cce7499b97d7b293363039df41919b3","datavalue":{"value":{"amount":"+0.732075572013855","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":"Q2726307$1E4F3448-D88B-4F50-A5C5-154C9D3D394E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Tactic-based inductive theorem prover for data types with partial operations (Diss., Univ. Kaiserslautern, 1999)","badges":[]}}}}}