Jeremie Wajs  @ NUS Home/Search
Context Related
| cas.mcmaster.ca/~wajs...wajs02phd.ps.gz Cached: PS.gz PS PDF Image Update Help From: cas.mcmaster.ca/~wajs/res...index (more) (Enter author homepages) |
Rate this article:      (best)Comment on this article |
Abstract: In this dissertation, we exhibit work revolving around the FO meta-logic. After going over some of the background material on FO , we discuss work about induction, and give induction principles that are richer than mathematical induction, in that they yield shorter, simpler and more elegant proofs. We then define and study notions of entailment and equivalence between two FO definitions. We make use of these notions by defining a framework, closely related to FO , for performing... (Update)
Context of citations to this paper: More
...definitions. Jeremie Wajs and Miller have been developing a tactic style theorem prover for a logic with induction and definitions [Waj02]. This system, called Iris, is written entirely in Nadathur s Teyjus implementation [NM99] of #Prolog and appears to be the first theorem...
Cited by: More
A Logical Framework For Reasoning About Logical Specifications - Tiu (2004) (Correct)
Encoding Generic Judgments - Miller, Tiu (2002) (Correct)
Active bibliography (related documents): More All
0.8: Lógica Linear E a Especificação De Sistemas .. - Pimentel (2001) (Correct)
0.8: Unknown - (Correct)
0.6: Compiler Construction in Higher Order Logic Programming - Liang (2002) (Correct)
Similar documents based on text: More All
0.2: A Proof Theory for Generic Judgments - Miller, Tiu (2003) (Correct)
0.1: A Proof Search Specification of the π-Calculus - Tiu, Miller (2004) (Correct)
0.1: On the Difference between Abduction and Induction: A.. - Denecker, Martens, De.. (1996) (Correct)
Related documents from co-citation: More All
2: A higher-order specification of the #-calculus (context) - Despeyroux - 2000
2: Reasoning in a Logic with Definitions and Induction (context) - McDowell - 1997
2: Cut elimination for a logic with definitions and induction - McDowell, Miller - 1997
BibTeX entry: (Update)
Jeremie D. Wajs. Reasoning about Logic Programs Using Definitions and Induction. PhD thesis, Pennsylvania State University, 2002. 15 http://citeseer.comp.nus.edu.sg/668769.html More
@misc{ wajs02reasoning,
author = "J. Wajs",
title = "Reasoning about Logic Programs Using Definitions and Induction",
text = "Jeremie D. Wajs. Reasoning about Logic Programs Using Definitions and Induction.
PhD thesis, Pennsylvania State University, 2002. 15",
year = "2002",
url = "citeseer.comp.nus.edu.sg/668769.html" }
Citations (may not include all citations):3972 Introduction to algorithms (context) - Cormen, Leiserson et al. - 1990
638 Partial evaluation and automatic program generation (context) - Jones, Gomard et al. - 1993
484 A Calculus of Communicating Systems (context) - Milner - 1980
447 Prentice-Hall International (context) - Milner, Concurrency - 1989
385 A transformation system for developing recursive programs - Burstall, Darlington - 1977
266 Information and Computation (context) - Coquand, Huet et al. - 1988
257 Logic programming in a fragment of intuitionistic linear log.. - Hodas, Miller - 1994
251 A logic programming language with lambda-abstraction - Miller - 1991
174 A unification algorithm for typed -calculus (context) - Huet - 1975
168 Rippling: A heuristic for guiding inductive proofs - Bundy, Stevens et al. - 1993
146 Investigations into logical deductions (context) - Gentzen - 1969
143 The Coq proof assistant user's guide (context) - Dowek, Felty et al. - 1993
121 Intensional interpretations of functionals of finite type (context) - Tait - 1967
95 A basis for a mathematical theory of computation - McCarthy - 1963
62 Unfoldfold transformation logic program (context) - Tamaki, Unfold et al. - 1984
53 Implementing tactics and tacticals in a higher-order logic p.. - Felty - 1993
49 Inductive definitions in the system Coq --- rules and proper.. - Paulin-Mohring - 1993
48 Operationally-based theories of program equivalence - Pitts - 1997
48 A logic for reasoning with higher-order abstract syntax (context) - McDowell, Miller - 1997
38 System description: Proof planning in higher-order logic wit.. - Richardson, Smaill et al. - 1998
25 A type theoretical alternative to CUCH (context) - Scott - 1969
22 Rules of definitional reflection (context) - Schroeder-Heister - 1993
21 Hauptsatz for the intuitionistic theory of iterated inductiv.. (context) - Martin-Lof - 1971
19 Reasoning with higher-order abstract syntax in a logical fra.. (context) - McDowell, Miller - 2002
19 System description: Teyjus---a compiler and abstract machine.. (context) - Nadathur, Mitchell - 1999
18 Transformational logic program synthesis (context) - Sato, Tamaki - 1984
16 Forum: A multiple-conclusion specification language (context) - Miller - 1996
16 Reasoning in a Logic with Definitions and Induction (context) - McDowell - 1997
15 Cut elimination for a logic with definitions and induction - McDowell, Miller - 2000
14 Transformation of logic programs - Pettorossi, Proietti - 1998
10 Abstract syntax for variable binders: An overview (context) - Miller - 2000
9 A finitary version of the calculus of partial inductive defi.. - Eriksson - 1991
7 The use of explicit proof plans to guide inductive proofs (context) - Bundy - 1988
5 Prolog: An introduction to the language and its logic (context) - Miller - 2001
3 comlinearmailing list trafficwwwmail (context) - Girard, in et al. - 1992
2 Automating functional program transformation - Mottl - 2000
2 A deterministic shift-reduce parser generator for a logic pr.. - Liang - 2000
1 Preuves de programmes logiques par induction et coinduction (context) - Craciunescu - 2001
Documents on the same site (http://www.cas.mcmaster.ca/~wajs/research/index.html):
Trustable Communication Between Mathematics Systems - Carette, Farmer, Wajs (2003) (Correct)
Unknown - (Correct)
Online articles have much greater impact More about CiteSeer.IST at NUS Add search form to your site Submit documents Feedback
CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.