Crystal: Integrating structured queries into a tactic language
From MaRDI portal
Publication:2655333
DOI10.1007/S10817-009-9138-5zbMath1185.68618OpenAlexW2102947465MaRDI QIDQ2655333
Dominik Dietrich, Ewaryst Schulz
Publication date: 25 January 2010
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-009-9138-5
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A higher-order implementation of rewriting
- Organization, transformation, and propagation of mathematical knowledge in \(\Omega \)mega
- A proof-centric approach to mathematical assistants
- Computer supported mathematics with \(\Omega\)MEGA
- Lightweight relevance filtering for machine-generated resolution problems
- Proof assistants: history, ideas and future
- IMPS: An interactive mathematical proof system
- Isabelle/HOL. A proof assistant for higher-order logic
- Mathematical knowledge management in HELM
- CASL reference manual. The complete documentation of the common algebraic specification language.
- User interaction with the Matita proof assistant
- A Declarative Language for the Coq Proof Assistant
- REWRITING WITH STRATEGIES IN $\mathsf{ELAN}$: A FUNCTIONAL SEMANTICS
- The challenge of computer mathematics
- Automated Deduction – CADE-20
- Mechanizing Mathematical Reasoning
- Synthesizing Proof Planning Methods and Ω-Ants Agents from Mathematical Knowledge
- Information Retrieval and Rendering with MML Query
- Types for Proofs and Programs
- Mathematical Knowledge Management
This page was built for publication: Crystal: Integrating structured queries into a tactic language
