{"entities":{"Q688727":{"pageid":690576,"ns":120,"title":"Item:Q688727","lastrevid":63634500,"modified":"2026-04-11T14:30:08Z","type":"item","id":"Q688727","labels":{"en":{"language":"en","value":"Theo: An interactive proof development system"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 438465"}},"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":"Q688727$D8C4C3B0-3D0B-4335-9974-83A5D65679F3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3538fa5f212e33792a06b3221c34013818efc157","datavalue":{"value":{"text":"Theo: An interactive proof development system","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q688727$D0AB7B58-F921-4410-9BD4-012DD2E6E700","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6f62e08e4e8f0a7494388c9bb5c03ae7779cc38b","datavalue":{"value":"0784.68074","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q688727$B2D2B803-8CAD-40EF-9AF2-56E39906B3DE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7da35c2cd71b3c7f1903c214fd23fa125921536c","datavalue":{"value":"10.1007/BF01995105","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q688727$99E30425-E63C-44DA-8DF1-A1DE5F363A27","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7e18514c052906fdc7b4ca4d0942d5aaa597b9ba","datavalue":{"value":{"entity-type":"item","numeric-id":688726,"id":"Q688726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688727$8535F233-DA69-4856-A312-4472644B23D3","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e560271c921b84b65a9b7f0d3fa6830623f8af8b","datavalue":{"value":{"entity-type":"item","numeric-id":188629,"id":"Q188629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688727$190E0C17-5A2C-4653-B499-6959624B5926","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9a56fa44f05f9c865c2049cda281119f7946a004","datavalue":{"value":{"time":"+1993-11-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q688727$3F26A47D-9C1D-44AB-9CC1-96C4A30F21F9","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"c9ec2cebb8bc7cd04bed64ebcca6203bafa99c01","datavalue":{"value":"The paper presents the main features of THEO, the first Typol version of a new tactic driven theorem prover which aims to help the user in building appropriate proofs in an object logic by proving theorems or derived rules in a backward way using resolution rule. The whole formalism used here, is essentially based on Gentzen sequent system. The resolution rule is expressed as a pair of Typol rules which describe the proof step when an inference rule is applied to the currently processed sequent. The basic implemented tactics, all of them being valid tactics, allow the user to add any number of previous derived rules and to ask for application of a particular instantiation of an object inference rule. Some editing manipulations as cut and paste transform can be applied to the derived proofs. The execution of the program can be controlled using the debugging facilities offered by Typol. Some examples of object logics which are already implemented under the described system are presented in the final part of the paper. A series of comments about some related work and conclusion remarks are formulated here too.","type":"string"},"datatype":"string"},"type":"statement","id":"Q688727$8FF7B32E-8002-4254-8209-A3F5A378C78F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q688727$AB997F57-8DCD-494B-A08D-BE3C31E06510","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q688727$1449ADCA-4821-4639-B041-999DB6A3DA7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"73dccdfb072fb026a86af92d74fe625efeb2b023","datavalue":{"value":"68T35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q688727$AD79098B-D334-4942-9C8D-44941930B38A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ca096c7f1a8d74feb931d5f14928e19e40ee5578","datavalue":{"value":"438465","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q688727$6872877B-86BB-4CD6-A53F-92D1B2AF9149","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fd1d0489a351c380aee48f056919469c50d1995b","datavalue":{"value":"logics and meaning of programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q688727$81E24324-3324-4971-8C3C-8B7C3B165234","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0e36fd2915ee69146bd208b73e1714d6ba9054ec","datavalue":{"value":"symbolic computation","type":"string"},"datatype":"string"},"type":"statement","id":"Q688727$66396B64-A675-4820-9E44-9DF44536AE21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q688727$4346C3A8-9E9A-451F-92C6-2045E072D8B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83d5dcaa7aef3dc9ddc3eab92a7db35d53442c07","datavalue":{"value":"proof theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q688727$EBFDCBE2-249E-4677-8244-C100373073F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"19d8846356e23b7db429d35ac4b09fde8a3a3752","datavalue":{"value":"tactic driven theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q688727$A5B546F7-9A9D-4499-A4C2-BCACF75772B4","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"00dcf12b9a602d9c5eb5566a233851af0f0ed4fd","datavalue":{"value":{"entity-type":"item","numeric-id":469832,"id":"Q469832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688727$8CDD2E5D-90E7-4E2C-8684-CF326A999ABE","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688727$85BB60C9-A36D-4F6D-9412-D535912CC0D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bab752e9cf98240487eb3aae10666dc541b36d41","datavalue":{"value":{"entity-type":"item","numeric-id":43692,"id":"Q43692"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688727$995565A3-9F3A-4D65-92EC-42B320DBB43A","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":"Q688727$82FCBA9B-A378-4228-B163-4507ACBAD417","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"70c434b6534caa8d7aae026f7b80e8e45e51931c","datavalue":{"value":{"entity-type":"item","numeric-id":809992,"id":"Q809992"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688727$DD401523-D651-4BC7-AB5A-375F07335864","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f7c99e107348aa82bd1ed9ca721c57c6ffc4f86","datavalue":{"value":{"entity-type":"item","numeric-id":688571,"id":"Q688571"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688727$F6E04A80-2A64-44E0-988A-ADFED9E5DF6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5e2b13fd5a27d330f592699f5bb5ff339813ded","datavalue":{"value":{"entity-type":"item","numeric-id":3789101,"id":"Q3789101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688727$2B0A0B70-6575-4330-AE62-4F4E85987975","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ff1c9576a9af1e44009a9ef9a0f7f22e091829d5","datavalue":{"value":{"entity-type":"item","numeric-id":5610986,"id":"Q5610986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688727$A62354FA-97BD-4601-A955-66640773EBAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688727$A1DF9545-D0AA-4154-A209-A7CF6C3CB263","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"573c6c41ed26aa070e75225c6352a26e064dd624","datavalue":{"value":{"entity-type":"item","numeric-id":3774923,"id":"Q3774923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688727$FE484255-4455-44AC-9213-DFB9360C8207","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"777f1902a1127b94884ae1ddc89768860f054a6e","datavalue":{"value":{"entity-type":"item","numeric-id":3789060,"id":"Q3789060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688727$0B51C57A-E561-44AF-AA59-DFF46B77EA08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1404903fbb3450c69ae4b46e148487834232fe43","datavalue":{"value":{"entity-type":"item","numeric-id":1823013,"id":"Q1823013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688727$332E6A95-A7AC-4A94-B7AC-B83EEAF5E9B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d95625ec9e5b7c46cee42d87256157d982706a","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688727$429A6EEC-4D0C-40D8-AC26-5A4350951358","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ed6186f00d683b4c7cb7f70af7a03fd2b654c87","datavalue":{"value":{"entity-type":"item","numeric-id":5632554,"id":"Q5632554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q688727$E0D9CD83-C332-47BE-A9D5-4AE9FB412950","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"403c8b0cbd523f0c8413209604e7114bc3693db2","datavalue":{"value":"https://doi.org/10.1007/bf01995105","type":"string"},"datatype":"url"},"type":"statement","id":"Q688727$778402C3-6150-4781-BC31-02EF42B51BBE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b1e10f5b23071d0125fd77b8e4712da68e7b565f","datavalue":{"value":"W1970894287","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q688727$3944EB97-1D5D-46BE-9859-016408CF6587","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12aefa9b4d1ac07f2cec158784e90fbc89bd6230","datavalue":{"value":{"entity-type":"item","numeric-id":1189726,"id":"Q1189726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4bbc450732cf549a9b9275b83765bc179f32f244","datavalue":{"value":{"amount":"+0.7773059010505676","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":"Q688727$86715AAD-431D-4046-873C-94AA0958A1BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f62d3c74f1452c00e4d697b29b4b03afa7c01b35","datavalue":{"value":{"entity-type":"item","numeric-id":865629,"id":"Q865629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9cde00bedf60370504ab8d4ea19b08a8484b30b1","datavalue":{"value":{"amount":"+0.769923210144043","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":"Q688727$86943D34-0ABA-4893-8A82-DC15D2348DF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9309577822db3b21e2b3a967403d44aa61bb595b","datavalue":{"value":{"entity-type":"item","numeric-id":5387844,"id":"Q5387844"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d4b55e527b291fafd8d8df95c40ed3ebb0e0e242","datavalue":{"value":{"amount":"+0.7667049765586853","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":"Q688727$675820C4-AF5E-47C8-9E2A-A5E5E9898B02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cb5b9cb0856d127c2a916c295ebc1e9c91730609","datavalue":{"value":{"entity-type":"item","numeric-id":3804241,"id":"Q3804241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3953565db76a95e4dd2f52c37340d381b53bcf0f","datavalue":{"value":{"amount":"+0.7654430270195007","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":"Q688727$1A28FFEA-D9A8-433A-8A3F-246C6F669540","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d8229f7daafb1debae26fdffd7e93734038545a","datavalue":{"value":{"entity-type":"item","numeric-id":5210800,"id":"Q5210800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"45bd92560983a2153d43feca11ebef97f88ca3cb","datavalue":{"value":{"amount":"+0.7520967721939087","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":"Q688727$A6B24A67-17F6-4C28-9C3E-EA1D9C5DC139","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Theo: An interactive proof development system","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Theo:_An_interactive_proof_development_system"}}}}}