Ωmega: Towards a mathematical assistant

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

Mathematics Subject Classification ID

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

• OTTER
• PROVERB
• Omega-MKRP

Cites Work

• Integrating computer algebra into proof planning
• Presenting machine-found proofs
• Unnamed Item