Автоматическое доказательство

Автоматическое доказательство (англ. Automated Theorem Proving, ATP, а также Automated deduction) — доказательство, реализованное программно. В основе лежит аппарат математической логики. Используются идеи теории искусственного интеллекта. Процесс доказательства основывается на логике высказываний и логике предикатов.

В силу неразрешимости даже достаточно простых теорий практическое применение имеет лишь полуавтоматическое человеко-машинное доказательство. К тому же после полной автоматизации доказательство называют уже вычислением. Полностью автоматической может быть лишь проверка доказательства теорий посложнее (если его для этого подготовить).

Применение

В настоящее время автоматическое доказательство теорем в промышленности применяется в основном при разработке и верификации интегральных схем и программного обеспечения. После того, как была обнаружена ошибка деления в процессорах Пентиум, сложные модули операций с плавающей запятой современных микропроцессоров разрабатываются с особой тщательностью. В новых процессорах AMD, Intel и других фирм автоматическое доказательство теорем используется для проверки того, что деление и другие операции выполняются корректно.

Корпорация Microsoft использует автоматический доказатель теорем Z3 для верификации кода операционной системы Windows 7 и других программных продуктов[1].

Примеры

См. также

Примечания

  1. Gwen Salaün, Bernhard Schätz. Formal Methods for Industrial Critical Systems: 16th International Workshop, FMICS 2011, Trento, Italy, August 29-30, 2011, Proceedings. — Springer, 2011. — P. 5. — ISBN 9783642244308.

Ссылки

Read other articles:

Krems II Lambang kebesaranLetak Krems II di Segeberg NegaraJermanNegara bagianSchleswig-HolsteinKreisSegeberg Municipal assoc.Leezen Pemerintahan • MayorHolger Möller (CDU)Luas • Total8,45 km2 (326 sq mi)Ketinggian19 m (62 ft)Populasi (2013-12-31)[1] • Total440 • Kepadatan0,52/km2 (1,3/sq mi)Zona waktuWET/WMPET (UTC+1/+2)Kode pos23829Kode area telepon04552Pelat kendaraanSESitus webwww.amt-leezen.de Kre...

 

 

Draško Mrvaljević Mrvaljević pada 2011Personal informationNama lengkap Draško MrvaljevićLahir 17 November 1979 (umur 44)Cetinje,  MontenegroKebangsaan MontenegroTinggi 192 m (629 ft 11 in)Posisi permainan Tengah belakangKlub seniorTahun Tim1997–2000 Lovćen2000–2002 Sintelon2003–2005 Teucro2005–2007 Torrevieja2007–2009 Koper2009–2012 Frisch Auf Göppingen2012–2013 Bregenz2013–2014 GWD Minden2014–2015 Hapoel Rishon LeZion2015–2016 SG Pforzheim/...

 

 

Judul yang benar dari artikel ini adalah Formula of Love: O+T=<3. Penggantian atau pengabaian tanda kurung karena keterbatasan teknis. Formula of Love: O+T=<3Sampul Digital dan versi Study About LoveAlbum studio karya TwiceDirilis12 November 2021 (2021-11-12)StudioJYPE Studios (Seoul)GenreK-popDurasi48:31BahasaKoreaInggrisLabel JYP Republic Kronologi Twice Perfect World(2021) Formula of Love: O+T=<3(2021) #Twice4(2022) Singel dalam album Formula of Love: O+T=<3 The Fee...

Pour les articles homonymes, voir La Croix (homonymie) et Croix. La Croix Pays France Langue Français Périodicité Quotidien Format Tabloïd Genre Généraliste Prix au numéro 2,90 €[1] Diffusion 91 762[2] ex. (2022, -3,48%) Date de fondation 15 juin 1883 (il y a 140 ans) Ville d’édition Paris Propriétaire Groupe Bayard Presse Directeur de publication Pascal Ruffenach Directeur de la rédaction Anne Ponce Rédacteur en chef Dominique Greiner, Jean-Christophe Ploquin, Isabe...

 

 

Festival of the people of Winneba The Aboakyer festival is a bushbuck hunting festival celebrated by the people of Winneba in the Central Region of Ghana.[1] Overview These men catches deer to celebrate Aboakyer festival in Ghana The name Aboakyer translates as hunting for game or animal in the Fante dialect as spoken by the people of the Central Region. The institution of the festival was to commemorate the migration of Simpafo (traditional name given to the people of Winneba). The p...

 

 

Université du WyomingHistoireFondation 1886StatutType Université publiqueNom officiel University of WyomingRégime linguistique Anglais américainPrésident Tom BuchananMembre de ORCID (d), Digital Library Federation (en), Wyoming Nonprofit Network (d)Site web www.uwyo.eduChiffres-clésÉtudiants 13 992 (en 2012)Effectif 2 908 (2020)LocalisationPays États-UnisVille LaramieLocalisation sur la carte des États-UnisLocalisation sur la carte du Wyomingmodifier - modifier le code - mo...

NASA space program which sent frogs into orbit Orbiting Frog OtolithThe Orbiting Frog Otolith (OFO) spacecraftMission typeBioscienceOperatorNASACOSPAR ID1970-094ASATCAT no.04690Mission duration6 days Spacecraft propertiesManufacturerAmes Research CenterLaunch mass132.9 kilograms (293 lb)Dimensions1.68 × 0.76 m (5.5 × 2.5 ft) Start of missionLaunch date9 November 1970, 06:00:00 (1970-11-09UTC06Z) UTCRocketScout B S174CLaunch siteWallops LA-3A End ...

 

 

クルアーンのスーラについては「地震 (クルアーン)」をご覧ください。 ポータル 災害 地震(じしん、英: earthquake)は、以下の2つの意味で用いられる[1]。 地震学における定義: 地球表面を構成している岩盤(地殻)の内部で、固く密着している岩石同士が、断層と呼ばれる破壊面を境目にして、急激にずれ動くこと。これによって大きな地面の振動が生じ�...

 

 

Korean noodle dish in soy milk broth Kong-guksuAlternative namesNoodles in cold soybean soupTypeGuksuCourseColdPlace of originKoreaMain ingredientsNoodles (wheat flour), soybean soupFood energy(per 1 serving)110 kcal (461 kJ)[1]  Media: Kong-guksu Korean nameHangul콩국수Revised Romanizationkong-guksuMcCune–Reischauerk'ong-guksuIPA[kʰoŋ.ɡuk̚.s͈u] Kong-guksu made from Paju jangdan beans Kong-guksu[2] (콩국수) or noodles in cold soybean sou...

Electromechanical switch A high-voltage (left) and a medium-voltage disconnector (right) Electrical installations Wiring practice by region or country North American practice United Kingdom practice Regulation of electrical installations BS 7671 UK wiring regulations IEC 60364 IEC international standard Canadian Electrical Code (CE Code) U.S. National Electrical Code (NEC) Cabling and accessories AC power plugs and sockets Cable tray Electrical conduit Mineral-insulated copper-clad cable Mult...

 

 

此条目序言章节没有充分总结全文内容要点。 (2019年3月21日)请考虑扩充序言,清晰概述条目所有重點。请在条目的讨论页讨论此问题。 哈萨克斯坦總統哈薩克總統旗現任Қасым-Жомарт Кемелұлы Тоқаев卡瑟姆若马尔特·托卡耶夫自2019年3月20日在任任期7年首任努尔苏丹·纳扎尔巴耶夫设立1990年4月24日(哈薩克蘇維埃社會主義共和國總統) 哈萨克斯坦 哈萨克斯坦政府...

 

 

The Right HonourableSaara Kuugongelwa-AmadhilaMP Perdana Menteri Namibia ke-4PetahanaMulai menjabat 21 Maret 2015PresidenHage GeingobWakilNetumbo Nandi-NdaitwahPendahuluHage GeingobPenggantiPetahanaMenteri KeuanganMasa jabatan2003 – 21 Maret 2015PresidenSam NujomaHifikepunye PohambaHage GeingobPendahuluNangolo MbumbaPenggantiCalle SchlettweinDirektur Jenderal Komisi Perencanaan Nasional NamibiaMasa jabatan1995–2003PresidenSam NujomaPenggantiImmanuel Ngatjizeko Informasi priba...

Italian association football club Football clubCataniaFull nameCataniaFootball Club s.r.l.[1][2]Nickname(s)I Rossazzurri (The Red and Blues) Gli Elefanti (The Elephants)Gli Etnei (The Etneans)Founded1929; 95 years ago (1929)GroundStadio Angelo Massimino,Catania, ItalyCapacity23,266[3]OwnerElefante 1946 Pty Ltd (Pelligra Group)ChairmanRoss PelligraCoachMichele ZeoliLeagueSerie C Group C2022–23Serie D Group I, 1st of 18 (promoted)WebsiteClub website H...

 

 

British independent record company This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these template messages) This article contains content that is written like an advertisement. Please help improve it by removing promotional content and inappropriate external links, and by adding encyclopedic content written from a neutral point of view. (August 2017) (Learn how and when to remove this message) This article may ha...

 

 

DarlingSingle by PoacherReleased1978Length3:18Label Carrere Republic RK Songwriter(s)Oscar Stewart BlandamerProducer(s)Barry Kingston Darlin' is a song written in 1970 by English sax player Oscar Stewart Blandamer. It was first released under the title Darling by the British country band Poacher in 1978. It was later a chart hit for Frankie Miller and David Rogers. The track was subsequently recorded by numerous artists including Tom Jones, Barbara Mandrell, Smokie and Johnny Reid. Background...

County in Pennsylvania, United States County in PennsylvaniaLackawanna CountyCountyLackawanna County Courthouse in Scranton in August 2009 FlagSealLocation within the U.S. state of PennsylvaniaPennsylvania's location within the U.S.Coordinates: 41°26′N 75°37′W / 41.44°N 75.61°W / 41.44; -75.61Country United StatesState PennsylvaniaFoundedAugust 13, 1878Named forLackawanna River[1]SeatScrantonLargest cityScrantonArea • Total465 ...

 

 

Artikel ini perlu diwikifikasi agar memenuhi standar kualitas Wikipedia. Anda dapat memberikan bantuan berupa penambahan pranala dalam, atau dengan merapikan tata letak dari artikel ini. Untuk keterangan lebih lanjut, klik [tampil] di bagian kanan. Mengganti markah HTML dengan markah wiki bila dimungkinkan. Tambahkan pranala wiki. Bila dirasa perlu, buatlah pautan ke artikel wiki lainnya dengan cara menambahkan [[ dan ]] pada kata yang bersangkutan (lihat WP:LINK untuk keterangan lebih lanjut...

 

 

この項目では、一級河川の勝田川について説明しています。そのほかの河川および用法については「勝田川 (曖昧さ回避)」をご覧ください。 勝田川 さかえ橋付近水系 一級水系 利根川種別 一級河川延長 約8.3 km流域面積 20.24 km²水源 千葉市稲毛区小深町付近水源の標高 29 m河口・合流先 印旛放水路(八千代市)流域 千葉市稲毛区・四街道市・千葉市花見川区・佐倉�...

South Korean singer (born 1989) In this Korean name, the family name is Kim. Kim Hyo-yeonKim in March 2022Born (1989-09-22) September 22, 1989 (age 34)Incheon, South KoreaOccupationsSingerdancerDJtelevision personalityMusical careerGenresK-popEDMInstrument(s)VocalsYears active2007–presentLabelsSMScreaM RecordsMember ofGirls' GenerationGirls' Generation-Oh!GGSM TownGot the BeatFormerly ofYounique UnitTriple TWebsiteOfficial website Musical artistKorean nameHangul김효연Hanja金孝淵R...

 

 

South African media group For the American company formerly known as Primedia, see RentPath. For infomercial company, see PriMedia Inc. This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these template messages) This article relies excessively on references to primary sources. Please improve this article by adding secondary or tertiary sources. Find sources: Primedia – news · newspapers �...