rdfs:comment
| - Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science. (en)
- Teoremen frogapen automatikoa (ingelesez Authomathed theorem proving edo ATP) azpialorra da eta programa informatikoen bidez teorema matematikoak frogatzeaz arduratzen da. (eu)
- 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. (es)
- La démonstration automatique de théorèmes (DAT) est l'activité d'un logiciel qui démontre une proposition qu'on lui soumet, sans l'aide de l'utilisateur. (fr)
- 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. (it)
- 자동정리증명(自動定理證明, Automated theorem proving, ATP) 또는 자동 연역(Automated deduction)은 자동 추론 연구의 한 분야로, 수학적 정리들을 컴퓨터 프로그램을 통해 형식적으로 증명하는 것, 또는 그에 대한 연구를 가리킨다. (ko)
- 自動定理証明(英: automated theorem proving, ATP)とは、自動推論 (AR) の中でも最も成功している分野であり、コンピュータプログラムによって数学的定理に対する証明を発見すること。ベースとなる論理によって、定理の妥当性を決定する問題は簡単なものから不可能なものまで様々である。 (ja)
- Automatyczne dowodzenie twierdzeń (ang. automated theorem proving) – 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. Dla komputera wygodniejsze jest zwykle wnioskowanie w tył, choć czasem stosuje się też wnioskowanie w przód. Przykładem twierdzenia, które zostało dowiedzione dopiero przez ATP jest "Algebry Robbinsa są boolowskie". (pl)
- Prova automática de teoremas (PAT) ou dedução automática (DA) é a prova de teoremas matemáticos por um programa de computador. É atualmente a sub-área mais desenvolvida do raciocínio automatizado (RA). (pt)
- Demonstração automatizada de teoremas (cuja sigla em inglês é ATP, ou dedução automática) é um sub-campo da área da Ciência da Computação e da Lógica que lida com o problema de provar teoremas matemáticos através de programas de computador. O raciocínio automatizado para uma demonstração matemática foi uma das áreas de maior interesse e ímpeto para o desenvolvimento da ciência dos computadores. (pt)
- 自動化定理證明(Automated theorem proving,簡稱ATP)目前是自动推理(Automated reasoning,簡稱AR)体系中发展最好的部分,它的目的是为使用电子计算机程序来进行数学定理的证明。对于不同的公理系统,它能够推论出一个定理在此系统下是正确的,还是不可证明的,或者错误的。 (zh)
- Автоматичне доведення (англ. Automated theorem proving) — доведення, реалізоване на програмному рівні. В основу покладено апарат математичної логіки. Використовуються ідеї теорії штучного інтелекту. Процес доведення базується на численні висловлень і логіці предикатів. В силу нерозв'язності навіть достатньо простих теорій практичне застосування має лише напівавтоматичне людсько-машинне доведення. До того ж після повної автоматизації доведення називають вже обчисленням. Повністю автоматичною може бути лише перевірка доведення більш складних теорій (якщо його для цього підготувати). (uk)
- Автоматическое доказательство (англ. Automated Theorem Proving, ATP, а также Automated deduction) — доказательство, реализованное программно. В основе лежит аппарат математической логики. Используются идеи теории искусственного интеллекта. Процесс доказательства основывается на логике высказываний и логике предикатов. (ru)
|