Ωmega: Towards a mathematical assistant
From MaRDI portal
Publication:5234706
DOI10.1007/3-540-63104-6_23zbMath1430.68393OpenAlexW1491353074MaRDI QIDQ5234706
Volker Sorge, Andreas Meier, Wolf Schaarschmidt, Detlef Fehrer, Lassaad Cheikhrouhou, Manfred Kerber, Michael Kohlhase, Karsten Konrad, Armin Fiedler, Xiaorong Huang, Christoph Benzmüller, Erica Melis, Jörg H. Siekmann
Publication date: 1 October 2019
Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-63104-6_23
Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
SAD as a mathematical assistant -- how should we go from here to there?, Supporting the formal verification of mathematical texts, Dealing with algebraic expressions over a field in Coq using Maple, Knowledge-based proof planning, Agenda control for heterogeneous reasoners, MBase: Representing knowledge and context for the integration of mathematical software systems, TacticToe: learning to prove with tactics, OMEGA, Presenting inequations in mathematical proofs, Plagiator — A learning prover, Web Interfaces for Proof Assistants
Uses Software
Cites Work