| dbo:abstract |
La demostración interactiva de teoremas es un campo de la ciencia computacional y la lógica matemática relativo a las herramientas para desarrollar pruebas formales para la colaboración hombre-máquina. Esto involucra una especie de asistente de pruebas: un editor interactivo de pruebas, u otra interfaz, con la cual un hombre pueda guiar la búsqueda de pruebas, los detalles que están almacenadas en ellas, y algunos de los pasos ofrecidos por, un ordenador. Ejemplos: * (por ejemplo, Isabelle) * (PVS) * Coq * PhoX * (es) En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques, soit sur des assertions relatives à l'exécution de programmes informatiques. (fr) In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer. (en) System wspomagający dowodzenie twierdzeń (ang. proof assistant, interactive theorem prover) – program komputerowy pozwalający użytkownikowi na zapis wyrażeń i formuł matematycznych oraz pomagający przy przeprowadzaniu ich dowodu. W ogólności automatyczne dowodzenie twierdzeń jest niemożliwe, gdyż dla wielu logik pytanie, czy dana formuła ma dowód jest nierozstrzygalne, dlatego provery zazwyczaj tylko asystują użytkownikowi przy przeprowadzaniu dowodu i weryfikują, czy użytkownik nie wykonuje niedozwolonych operacji. Zwykle potrafią również znaleźć dowody dla prostych faktów lub udzielić użytkownikowi wskazówek, które drogi rozumowania mogą doprowadzić do wyniku, niemniej ich moc jest ograniczona. Przykładowe provery: * * * * Mizar * (PVS) Przykładowe dowody używające proverów: * twierdzenie o czterech barwach * Postulat Keplera (pl) Инструмент интерактивного доказательства теорем (интерактивный решатель теорем) — программное обеспечение, помогающее исследователю в разработке формальных доказательств.Доказательства вырабатываются в процессе взаимодействия человека с машиной. Как правило, такое программное обеспечения включает в себя какую-то разновидность интерактивного редактора доказательств или другой интерфейс, с помощью которого человек может вести поиск доказательств, сведения о которых хранятся в компьютере, а также процедуры автоматической проверки доказательств, осуществляемые компьютером. (ru) |
| rdfs:comment |
La demostración interactiva de teoremas es un campo de la ciencia computacional y la lógica matemática relativo a las herramientas para desarrollar pruebas formales para la colaboración hombre-máquina. Esto involucra una especie de asistente de pruebas: un editor interactivo de pruebas, u otra interfaz, con la cual un hombre pueda guiar la búsqueda de pruebas, los detalles que están almacenadas en ellas, y algunos de los pasos ofrecidos por, un ordenador. Ejemplos: * (por ejemplo, Isabelle) * (PVS) * Coq * PhoX * (es) En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques, soit sur des assertions relatives à l'exécution de programmes informatiques. (fr) In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer. (en) Инструмент интерактивного доказательства теорем (интерактивный решатель теорем) — программное обеспечение, помогающее исследователю в разработке формальных доказательств.Доказательства вырабатываются в процессе взаимодействия человека с машиной. Как правило, такое программное обеспечения включает в себя какую-то разновидность интерактивного редактора доказательств или другой интерфейс, с помощью которого человек может вести поиск доказательств, сведения о которых хранятся в компьютере, а также процедуры автоматической проверки доказательств, осуществляемые компьютером. (ru) System wspomagający dowodzenie twierdzeń (ang. proof assistant, interactive theorem prover) – program komputerowy pozwalający użytkownikowi na zapis wyrażeń i formuł matematycznych oraz pomagający przy przeprowadzaniu ich dowodu. W ogólności automatyczne dowodzenie twierdzeń jest niemożliwe, gdyż dla wielu logik pytanie, czy dana formuła ma dowód jest nierozstrzygalne, dlatego provery zazwyczaj tylko asystują użytkownikowi przy przeprowadzaniu dowodu i weryfikują, czy użytkownik nie wykonuje niedozwolonych operacji. Zwykle potrafią również znaleźć dowody dla prostych faktów lub udzielić użytkownikowi wskazówek, które drogi rozumowania mogą doprowadzić do wyniku, niemniej ich moc jest ograniczona. (pl) |
