| German |
| has gloss | deu: Als Computerbeweis bezeichnet man den Beweis einer Behauptung, das heißt einer mathematischen oder logischen Aussage, mit Hilfe eines Computerprogramms. |
| lexicalization | deu: Computerbeweis |
| Persian |
| has gloss | fas: اثبات قضیه خودکار در علوم رایانه به بررسی راه‌های ممکن برای اثبات قضیه‌ها به صورت خودکار (معمولا با برنامه کامپیوتری) می‌پردازد. اثبات قضیه خودکار یکی از مهم‌ترین شاخه‌های استدلال خودکار به شمار می‌آید، اما همچنین به مقدار زیادی به علوم رایانه نظری و فلسفه مربوط است. منظور از قضیه در این‌جا قضیه ریاضی است. |
| lexicalization | fas: اثبات قضیه خودکار |
| French |
| has gloss | fra: La démonstration automatique de théorèmes est lactivité dun logiciel qui démontre une proposition quon lui soumet sans laide de l'utilisateur. |
| lexicalization | fra: Demonstration automatique de theoremes |
| lexicalization | fra: Démonstrateur automatique de théorèmes |
| lexicalization | fra: Démonstration automatique de théorèmes |
| Italian |
| has gloss | ita: La dimostrazione automatica di teoremi (in inglese Automated theorem proving o ATP) o deduzione automatica, è il sottocampo più sviluppato del ragionamento automatico. L'operazione consiste nella dimostrazione di teoremi matematici da parte di un programma per computer. |
| lexicalization | ita: Dimostrazione automatica di teoremi |
| Japanese |
| has gloss | jpn: 自動定理証明（Automated Theorem Proving、ATP）とは、自動推論(AR) の中でも最も成功している分野であり、コンピュータプログラムによって数学的定理を証明すること。ベースとなる論理によって、定理の妥当性を決定する問題は簡単なものから不可能なものまで様々である。 |
| lexicalization | jpn: 自動定理証明 |
| Polish |
| has gloss | pol: Automatyczne dowodzenie twierdzeń (ang. automated theorem proving) to proces, w którym komputer rozstrzyga czy dane twierdzenie jest dowodliwe w jakiejś teorii, często przy okazji generując jego dowód. Twierdzenia te należą zwykle do rachunku zdań lub rachunku predykatów pierwszego rzędu. |
| lexicalization | pol: Automatyczne dowodzenie twierdzeń |
| Portuguese |
| has gloss | por: Prova automática de teoremas (PAT) ou dedução automática é a prova de teoremas matemáticos por um programa de computador. É atualmente a sub-área mais desenvolvida do raciocínio automatizado (RA). |
| lexicalization | por: Prova automática de teoremas |
| Russian |
| has gloss | rus: Автоматическое доказательство теорем — доказательство теорем, реализуемое программно. В основе лежит аппарат математической логики. Используются идеи теории искусственного интеллекта. Процесс доказательства основывается на логике высказываний и логике предикатов. |
| lexicalization | rus: автоматическое доказательство теорем |
| Castilian |
| has gloss | spa: La demostración automática de teoremas (de siglas ATP, por el término en inglés : Automated theorem proving) que también puede ser denominada Deducción automatizada, es actualmente el subcampo más desarrollado del razonamiento automático, y se encarga de la demostración de teoremas matemáticos mediante programas de ordenador. |
| lexicalization | spa: Demostracion automatica de teoremas |
| lexicalization | spa: demostración automática de teoremas |
| Thai |
| has gloss | tha: การพิสูจน์ทฤษฎีบทด้วยคอมพิวเตอร์ เป็นบทพิสูจน์ทฤษฎีทางคณิตศาสตร์ที่มีบางส่วนถูกสร้างขึ้นโดยคอมพิวเตอร์ |
| lexicalization | tha: การพิสูจน์ทฤษฎีบทด้วยคอมพิวเตอร์ |
| Chinese |
| has gloss | zho: 自動定理證明 (ATP), 目前是自动推理(AR)体系中发展最好的部分，它的目的是为使用电子计算机程序来进行数学定理的证明。对于不同的数学逻辑，它能够推论出一个定理是正确的，还是不可证明的，或者错误的。 |
| lexicalization | zho: 自動定理證明 |
