Access the full text.
Sign up today, get an introductory month for just $19.
Matt Kaufmann (1992)
An extension of the Boyer-Moore Theorem Prover to support first-order quantificationJournal of Automated Reasoning, 9
M. Gordon (1988)
HOL: A Proof Generating System for Higher-Order Logic
D. Plaisted, Richard Potter (1988)
Term Rewriting: Some Experimental Results
(1984)
After 25 Years, pp
S. Bailin, Dave Barker-Plummer (1993)
−-match: An inference rule for incrementally elaborating set instantiationsJournal of Automated Reasoning, 11
Finally, we prove the Theorem itself This involves performing the double induction, invoking lemmas for the base cases and induction step: i 2 nat j 2 nat 9 n2nat Ramsey(n; i; j) References
D. Prawitz (1971)
Ideas and Results in Proof TheoryStudies in logic and the foundations of mathematics, 63
Bengt Nordström, Kent Petersson, Jan Smith (1990)
Programming in Martin-Lo¨f's type theory: an introduction
(1992)
the sieve of Eratosthenes', in B
F. Pelletier (1986)
Seventy-five problems for testing automatic theorem proversJournal of Automated Reasoning, 2
G. Huet (1975)
A Unification Algorithm for Typed lambda-CalculusTheor. Comput. Sci., 1
(1992)
Ontic: Language speciication and user's manual
P. Halmos (1961)
Naive Set Theory
(1992)
The EVES library
D. Basin, Matt Kaufmann (1991)
The Boyer-Moore Prover and Nuprl: an experimental comparison
(1986)
Clauses for G6del's axioms', J
W. Bledsoe (1977)
Non-Resolution Theorem ProvingArtif. Intell., 9
M. Saaltink, Sentot Kromodimoeljo, Bill Pase, D. Craigen, I. Meisels (1993)
An EVES Data Abstraction Example
G. P. Huet (1975)
A unification algorithm for typed λ-calculusTheor. Computer Sci., 1
(1993)
The Isabelle reference manual. Technical Report
B. Graham (1992)
The SECD Microprocessor
D. Pastre (1978)
Automatic Theorem Proving in Set TheoryArtif. Intell., 10
C. Torrance (1941)
Review: Kurt Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis with the Axioms of Set TheoryBulletin of the American Mathematical Society, 47
S. Bailin (1988)
A λ-unifiability test for set theoryJournal of Automated Reasoning, 4
T. Melham, Juanito Camilleri, Ifip Tc (1994)
Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop, Valletta, Malta, September 19-22, 1994. Proceedings
(1990)
Collected Works, Vol
Lawrence Paulson, Krzysztof Grabczewski (1996)
Mechanizing set theoryJournal of Automated Reasoning, 17
Bengt Nordström, Kent Petersson, Jan Smith (1990)
Programming in Martin-Löf's Type Theory
(1986)
Journal of automated reasoningActa Applicandae Mathematica, 6
Peter Andrews, D. Miller, E. Cohen, F. Pfenning (1984)
AUTOMATING HIGHER-ORDER LOGIC
T. Melham, Juanito Camilleri (1994)
Higher Order Logic Theorem Proving and Its Applications, 859
T. Nipkow (1991)
Constructive RewritingComput. J., 34
D. McCarty (1985)
Realizability and recursive mathematics
Lawrence Paulson (1989)
The foundation of a generic theorem proverJournal of Automated Reasoning, 5
Lawrence Paulson (1999)
Introduction to Isabelle
K. Devlin (1979)
Fundamentals of contemporary set theory
R. Boyer, E. Lusk, W. McCune, R. Overbeek, M. Stickel, L. Wos (1986)
Set theory in first-order logic: Clauses for Gödel's axiomsJournal of Automated Reasoning, 2
Lawrence Paulson (1995)
Set theory for verification. II: Induction and recursionJournal of Automated Reasoning, 15
P. Suppes (1969)
Axiomatic set theory
K. Kunen (1983)
Set theory - an introduction to independence proofs, 102
F. Brown (1978)
Towards the Automation of Set Theory and its LogicArtif. Intell., 10
S. Thompson (1991)
Type theory and functional programming
M. Gordon (1985)
Why higher-order logic is a good formalism for specifying and verifying hardware
(1977)
A maximal method for set variables in automatic theorem - proving
P. Noel (1993)
Experimenting with Isabelle in ZF set theoryJournal of Automated Reasoning, 10
(1963)
Combinatorial Mathematics
F. Leclerc, Christine Paulin-Mohring (1994)
Programming with Streams in Coq - A Case Study: the Sieve of Eratosthenes
W. Bledsoe, Guohui Feng (1993)
SET-VARJournal of Automated Reasoning, 11
J. McDonald, P. Suppes (1984)
Student use of an interactive theorem prover
D. Cantone (2015)
Decision procedures for elementary sublanguages of set theory: X. Multilevel syllogistic extended by the singleton and powerset operatorsJournal of Automated Reasoning, 7
D. Miller (1992)
Unification Under a Mixed PrefixJ. Symb. Comput., 14
S. Krantz (2002)
The Axioms of Set Theory
Mark Saaltink (1992)
TheEves library models
(1993)
Paulson . The Isabelle reference manual
L. Lamport (1994)
The temporal logic of actionsACM Trans. Program. Lang. Syst., 16
P. Cameron (1998)
Naïve set theory
Art Quaife (1992)
Automated deduction in von Neumann-Bernays-Gödel set theoryJournal of Automated Reasoning, 8
B. Graham (1992)
The Secd Microprocessor: A Verification Case Study
A. Felty (1991)
A Logic Program for Transforming Sequent Proofs to Natural Deduction Proofs
(1992)
Types considered harmful
K. Gödel (1938)
The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis.Proceedings of the National Academy of Sciences of the United States of America, 24 12
P. Aczel (1988)
Non-well-founded sets, 14
Lawrence Paulson (2000)
Isabelle: The Next 700 Theorem ProversArXiv, cs.LO/9301106
A logic for specification and verification is derived from the axioms of Zermelo-Fraenkel set theory. The proofs are performed using the proof assistant Isabelle. Isabelle is generic, supporting several different logics. Isabelle has the flexibility to adapt to variants of set theory. Its higher-order syntax supports the definition of new binding operators. Unknowns in subgoals can be instantiated incrementally. The paper describes the derivation of rules for descriptions, relations, and functions and discusses interactive proofs of Cantor's Theorem, the Composition of Homomorphisms challenge [9], and Ramsey's Theorem [5]. A generic proof assistant can stand up against provers dedicated to particular logics.
Journal of Automated Reasoning – Springer Journals
Published: Dec 10, 2004
Read and print from thousands of top scholarly journals.
Already have an account? Log in
Bookmark this article. You can see your Bookmarks on your DeepDyve Library.
To save an article, log in first, or sign up for a DeepDyve account if you don’t already have one.
Copy and paste the desired citation format or use the link below to download a file formatted for EndNote
Access the full text.
Sign up today, get an introductory month for just $19.
All DeepDyve websites use cookies to improve your online experience. They were placed on your computer when you launched this website. You can change your cookie settings through your browser.