Computer supported mathematics with \(\Omega\)MEGA
From MaRDI portal
Publication:865650
DOI10.1016/j.jal.2005.10.008zbMath1107.68101OpenAlexW2141290989MaRDI QIDQ865650
Christoph Benzmüller, Serge Autexier, Jörg H. Siekmann
Publication date: 20 February 2007
Published in: Journal of Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jal.2005.10.008
artificial intelligenceproof planningcomputer-supported mathematicsinteractive and automated theorem-provingOmegaproof assistant systems
Related Items
The higher-order prover \textsc{Leo}-II, Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics, Proof planning with multiple strategies, Crystal: Integrating structured queries into a tactic language, Extensional higher-order paramodulation in Leo-III, Solving modal logic problems by translation to higher-order logic, Tactics for hierarchical proof, LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description), THF0 – The Core of the TPTP Language for Higher-Order Logic, Progress in the Development of Automated Theorem Proving for Higher-Order Logic, An Online Computing and Knowledge Platform for Differential Equations
Uses Software
Cites Work
- The seventeen provers of the world. Foreword by Dana S. Scott..
- Challenge problems in elementary calculus
- 9th international conference on automated deduction (CADE-9), Argonne, Illinois, USA, May 23-26, 1988. Proceedings
- The TPTP problem library. CNF release v1. 2. 1
- Artificial intelligence: methodology, systems, and applications. 8th international conference, AIMSA '98. Sozopol, Bulgaria, September 21--23, 1998. Proceedings
- Automated deduction - CADE-16. 16th international conference, Trento, Italy, July 7--10, 1999. Proceedings
- Automated deduction -- CADE-12. 12th international conference, Nancy, France, June 26 -- July 1, 1994. Proceedings
- Isabelle. A generic theorem prover
- Solution of the Robbins problem
- Automated deduction - CADE-15. 15th international conference, Lindau, Germany, July 5--10, 1998. Proceedings
- Comparing approaches to the exploration of the domain of residue classes.
- Automated deduction - CADE-17. 17th international conference, Pittsburgh, PA, USA, June 17--20, 2000. Proceedings
- Isabelle/HOL. A proof assistant for higher-order logic
- Constraint solving for proof planning
- TPS: A theorem-proving system for classical type theory
- Frontiers of combining systems. 3rd international workshop, FroCoS 2000, Nancy, France, March 22--24, 2000. Proceedings
- Knowledge-based proof planning
- Proof planning with multiple strategies
- Theoretical studies of sea animal locomotion, part 2
- Artificial Intelligence and Soft Computing - ICAISC 2004
- Automated Deduction – CADE-20
- Automated Deduction – CADE-20
- A Machine-Oriented Logic Based on the Resolution Principle
- Logic for Programming, Artificial Intelligence, and Reasoning
- Mechanizing Mathematical Reasoning
- Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings
- MBase: Representing knowledge and context for the integration of mathematical software systems
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
