Connecting a Logical Framework to a First-Order Logic Prover
- 1 January 2005
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
- p. 285-301
- https://doi.org/10.1007/11559306_17
Abstract
No abstract availableKeywords
This publication has 17 references indexed in Scilit:
- Connecting a Logical Framework to a First-Order Logic ProverLecture Notes in Computer Science, 2005
- Experiments on Supporting Interactive Proof Using ResolutionLecture Notes in Computer Science, 2004
- An LCF-Style Interface between HOL and First-Order LogicLecture Notes in Computer Science, 2002
- JProver: Integrating Connection-Based Theorem Proving into Interactive Proof AssistantsLecture Notes in Computer Science, 2001
- QuickCheckACM SIGPLAN Notices, 2000
- Integrating Gandalf and HOLLecture Notes in Computer Science, 1999
- Unification under a mixed prefixJournal of Symbolic Computation, 1992
- Automated reasoning about elementary point-set topologyJournal of Automated Reasoning, 1989
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965
- Untersuchungen ber das logische Schlie en. IIMathematische Zeitschrift, 1935