Connecting a Logical Framework to a First-Order Logic Prover
Authors:
- 1 January 2005
- book chapter
- Published by Springer Nature in Lecture Notes in Computer Science
- p. 285-301
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 Logic2002
- JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants2001
- QuickCheckACM SIGPLAN Notices, 2000
- Integrating Gandalf and HOL1999
- 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