{"entities":{"Q1189726":{"pageid":1200475,"ns":120,"title":"Item:Q1189726","lastrevid":70238196,"modified":"2026-04-13T13:24:40Z","type":"item","id":"Q1189726","labels":{"en":{"language":"en","value":"SETHEO: A high-performance theorem prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 57766"}},"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":"Q1189726$9501A0A2-3469-433A-83A1-D609D8DBDF24","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3ca8434c502388ab299a0a8d4d11106ffd48cdf7","datavalue":{"value":{"text":"SETHEO: A high-performance theorem prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1189726$4827667A-382A-4D75-AB8F-7D2D4EEE37D3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4dd395945b9b6652777c0f267104d1e23378b797","datavalue":{"value":"0759.68080","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1189726$54DE7FB1-1ECB-4E75-B2D4-2C945F4ABBC7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"135c0fdbace40a88a8d569c48bd80ba7102b3ea9","datavalue":{"value":"10.1007/BF00244282","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1189726$029F114F-9B4D-4FCC-838F-62E7101A0F71","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f5b17683dd2eedd3f1d821a1087aa218b2b31d17","datavalue":{"value":{"entity-type":"item","numeric-id":1160451,"id":"Q1160451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1189726$21900585-1B09-400E-BC54-BF440C650B56","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":"Q1189726$550BF58C-2939-4CE1-BA93-881215A8AB13","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5fd62271fe98c7ff9916cafed51cf35315eeeb31","datavalue":{"value":{"time":"+1992-09-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1189726$9203BA4D-A6D8-40C2-86AB-FD277AD9BB23","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"aba18aa1ca502e48c34f01d43a1d0902935aafa1","datavalue":{"value":"The paper deals with a theoretical background and practical knowledge of the implementation of the interesting system SETHEO --- a theorem prover for first order logic. The system is based on the connection method and is proved to be sound and complete. SETHEO can be used as an interpreter for the programming language LOP (under development). The inference machine of the system is implemented using Prolog technology, but there are some special characteristics differing SETHEO from common Prolog systems: a powerful preprocessing module for a reduction of the input formula, the proof procedure is realized as a WAM, factorization, lemma generation and the application of proof schemata are offered as options. The entire system is implemented in the language \\(C\\) and is running on several machines. The important feature of SETHEO is its performance of up to 70 Klips on a SUN SPARC station 1 with 12 Mips.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1189726$06FE677D-2865-4447-81F6-C9ACA32140B6","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"be2a52757c5af513b7fb2d5e98fbd88a4a770b60","datavalue":{"value":{"entity-type":"item","numeric-id":1188640,"id":"Q1188640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1189726$48CAF789-2A52-4803-9437-49FAD85A021E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1189726$3551E6B6-92C1-46F4-A8DC-13E4457C1B43","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cb8bb9656c1cd56bb6c7f1a12545f35f9a7d8904","datavalue":{"value":"57766","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1189726$9DA232D3-A4F1-4DF5-8400-2DC587335181","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6c98e3dc64270ec0de715f8b38eca46cbd549427","datavalue":{"value":"model elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q1189726$FD7E9CB0-34E0-4C6E-98A0-21324D90D71F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0ea7d27280984d745b55111c2fabcb2c69519735","datavalue":{"value":"abstract machine technology","type":"string"},"datatype":"string"},"type":"statement","id":"Q1189726$307F86B9-BAB5-4D0F-A4E3-538A57567684","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c39a3dcb919cfb7892b24ca37da2f18a4bcfe1c8","datavalue":{"value":"first order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1189726$4C1A174C-E650-453C-AD9A-E3ED35C70240","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9766ea21e04bbb663ab057ef2e9635b0fd3090d5","datavalue":{"value":"connection method","type":"string"},"datatype":"string"},"type":"statement","id":"Q1189726$658970CD-53BF-44F7-A896-A83218280A49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ff67fedbe8c50d3daca036875aed531217cd953b","datavalue":{"value":"Prolog","type":"string"},"datatype":"string"},"type":"statement","id":"Q1189726$6B32B395-6B8E-4579-928F-69654F34DD76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36957d7e632ee938df3990fd3662ec253f74cca5","datavalue":{"value":"preprocessing","type":"string"},"datatype":"string"},"type":"statement","id":"Q1189726$388199F3-7075-4B44-AE66-5F3D6F740267","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c845b927c7c8299e3e10848fbe9373f51ae3559b","datavalue":{"value":{"entity-type":"item","numeric-id":13461,"id":"Q13461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1189726$AFB34B90-B22A-4100-A841-A84E565C72A3","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":"Q1189726$99435E8F-00DE-40F7-BB13-B315E4099E2E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"57519cbbe51459d430d3d1fbc42fa6652e269278","datavalue":{"value":"https://doi.org/10.1007/bf00244282","type":"string"},"datatype":"url"},"type":"statement","id":"Q1189726$C7338501-D4BD-4165-ACC0-1920DE831D1B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"129b65464ca0f3363ee062a6ef0e8d995e673794","datavalue":{"value":"W2084894656","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1189726$4F21ECA2-82DC-4CB2-979D-80271DC022CB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"37e17781bce1ee102887185e1b39d38b59fe7e87","datavalue":{"value":{"entity-type":"item","numeric-id":6488521,"id":"Q6488521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e1affb93e2ca4fbd05fb08a3b6819658a3bea850","datavalue":{"value":{"amount":"+0.8319845795631409","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":"Q1189726$C88DB36E-367D-43E2-83B2-A12A5017A81E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"acc0626cd3fa6a38cbe12563c26e9aa91bb99318","datavalue":{"value":{"entity-type":"item","numeric-id":4524776,"id":"Q4524776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4ae5ea4a6a76a38244988b31d5b2e1fb0d5a1614","datavalue":{"value":{"amount":"+0.8140941858291626","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":"Q1189726$2170B040-C57F-4A59-95B8-4D8D89F83453","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f31b4a3d39713dc06eab1bc4b2bfc3409fd333dd","datavalue":{"value":{"entity-type":"item","numeric-id":1114446,"id":"Q1114446"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8a731af88ef1901004457d1465ec615a3593b86f","datavalue":{"value":{"amount":"+0.789833664894104","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":"Q1189726$CA4CF17B-0BFD-4D3A-8F1D-F71B6CFE13F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0e3cc3b3ee4f98cbf7948d48e3f76892dc00ca3b","datavalue":{"value":{"entity-type":"item","numeric-id":6488542,"id":"Q6488542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"62076a7d94ad2332da1fe466ae04bce94c5581ea","datavalue":{"value":{"amount":"+0.7828555107116699","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":"Q1189726$4462D4CC-FC40-48C0-8CAC-F897E7CCBF09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0456405130c3ea41f3a066f024f9d673ca3d1ec2","datavalue":{"value":{"entity-type":"item","numeric-id":3750142,"id":"Q3750142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"064b3f4f54617a2437006cf91017c47eedf163c8","datavalue":{"value":{"amount":"+0.7820544838905334","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":"Q1189726$41D181BD-AC1B-4880-B892-B9EA1AA325C9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"SETHEO: A high-performance theorem prover","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/SETHEO:_A_high-performance_theorem_prover"}}}}}