FOL Papers
1974
FOL: A proof checker for First Order Logic
Richard W. Weyhrauch and Arthur J. Thomas
AIM-235 and STAN CA 74-432 - these are identical
This was the first FOL manual. It contains a usage of the word 'context' on
page 2. It is a description of the logic of FOL which qiute clear. It
includes many examples, including axiomatizations of ZF and GBN.
1975
Checking Proofs in the Metamathematics of First Order Logic
Mario Aiello, Richard W. Weyhrauch
IJCAI 1975: 1-8
1976
An FOL primer
Filman, Robert E. and Weyhrauch, Richard W.
CS-TR-76-572
Stanford University, Department of Computer Science - September 1976
This primer is an introduction to FOL, an interactive proof checker
for first order logic. Its examples can be used to learn the FOL system, or
read independently for a flavor of our style of interactive proof checking.
Several example proofs are presented, successively increasing in the
complexity of the FOL commands employed.
ftp://reports.stanford.edu/pub/cstr/reports/cs/tr/76/572/CS-TR-76-572.pdf
1977
Weyhrauch, Richard W. (1977). FOL: A proof checker for first-order logic
(Stanford Artificial Intelligence Laboratory Memo AIM-235.1). Stanford
University, Stanford. A copy with this name cannot yet be found - It
seems to be superceded be the paper below
Weyhrauch, R.W., A Users Manual for FOL, Stanford AIM 235.1, 1977.
CS-TR-77.pdf
This PDF was made in some very strange way, I believe it was OCRed and then
converted to PDF. This is the only explaination for the strange rendering of
the fonts and the symbols used for quantifiers. The AI lab keyboards and
printers had the logic symbols on them and the papers we produced had them
accurately typeset, If possible get a copy of the original as it will have
much better topography. I will produce a PDF with images as my time permits.
Sorry.
1978
Prolegomena to a Theory of Mechanized Formal Reasoning
R.W. Weyhrauch
1) Stanford AI Memo AIM-315, 1978
2) Artificial Intelligence 13 (1980):133-170
also
3) Readings in Artificial Intelligence, ed. B.L. Webber and N.J. Nilsson
Morgan Kaufmann Publishers, Los Altos, CA, 1981 also
4) Readings in Knowledge Representation, ed. R. Brachman and H. Levesque,
Morgan Kaufmann Publishers, Los Altos, CA, 1985.
...
CS-TR-78-687
CS-TR-78-687
This paper is the most important academic publication relating to FOL.
It describes the notion of Language/Simulation pairs (L/S pairs) and
describes the finite data structures used to build them. It shows how to
define and use the finite description of a language plus recognizers for
sentences (ie WFFs) instead of infinite sets of formulas. It introduces
simulation structures, a finite computationl realization of the logicians
notion of model, and shows that, with respect to language/simulation
structure pairs (connected by what we called semantic attachment), you
can actually implement the logical notion of interpretation as a computer
program. This allows the definition of satisfaction in the usual way. This
provides finite reaalization notion of theory (which we called a context)
by adding a finite collection of 'facts' to an L/S pair. Because a context
can name another context and we can use semantic attachment connect this name
to the data structure for that context we get multi-context hierarchical
reasoning and metatheory 'for free'. We (and others) have used FOL contexts
to show how, simply using first order ideas (without the introduction of
'new' logics), you can do modal reasoning, reasoning about time without
indexicals, metatheory, reflection, non-monotonic logic, default reasoning,
circumscription, jumping to conclusions, ... . This paper has been reprinted
many times. The list does not contain them all.
1979
GOAL: A Goal Oriented Command Language for Interactive Proof Construction.
J.B. Bulnes-Rozas
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE.
STAN-CS-79-743AIM-328
This thesis described the theory and implemation of a system discuss proofs by
expressing the theorem you are interested as a goal and doing backward
chaining to find a proof. These "backward" steps today would likely be called
'abductive reasoning' but the abductions were directed by the user so there
was no search. Also the system used 'natural deduction' so the normalization
theorem told you what logical 'abductions' you had to do (but of course did
not 'solve' existentals for you. This frmework (as all of FOL) was a decendent of the LCF system of Milner and Weyhrauch [ref].
Abstract: This thesis represents a contribution to the development of
practical computer systems for interactive construction of formal proofs.
Beginning with a summary of current research in automatic theorem proving,
goal oriented systems, proof checking, and program verification, this work
aims at bridging the gap between proof checking and theorem proving.
Specifically, it describes a system GOAL for the First Order Logic proof
checker FOL. GOAL helps the user of FOL in the creation of long proofs in
three ways: (1) as a facility for structured, top down proof construction;
(2) as a semi-automatic theorem prover; and (3) as an extensible environment
for the programming of theorem proving heuristics. In GOAL, the user defines
top level goals. These are then recursively decomposed into subgoals. The main
part of a goal is a well formed formula that one desires to prove, but they
include assertions, simplification sets, and other Information. Goals can be
tried by three different types of elements: matchers, tactics, and strategies.
The matchers attempt to prove a goal directly - that is without reducing it
into subgoals - by calling decision procedures of FOL. Successful application
of a matcher causes the proved goal to be added to the FOL proof. A tactic
reduces a goal into one or more subgoals. The strategies are programmed
sequences of applications of tactics and matchers
1980
Using Meta-Theoretic Reasoning to do Algebra
Luigia Carlucci Aiello, Richard W. Weyhrauch
CADE 1980: 1-13
Final Report: Basic Research in Artificial Intelligence and Foundations of Programming
John McCarthy, et al edited by Lester Earnest
CS-TR-80-808
1982
R. Weyhrauch, An example of FOL using metatheory: Formalizing reasoning
systems and introducing derived inference rules, Proc. 6th Conf. on Automated
Deduction, ed. D. Loveland, LNCS 138, Springer-Verlag, Berlin, 1982,
pp. 151-158.
1988
F. Giunchiglia , R.W. Weyhrauch, A Multi-Context Monotonic Axiomatization of
Inessential Non-Monotonicity, Meta-Level Architectures and Reflection,
Editors: Pattie Maes, D. Nardi (1988) Reprinted 1991 A Multi-Context
Monotonic Axiomatization of Inessential Non-Monotonicity, F. Giunchiglia,
R.W. Weyhrauch, nonmon.pdf
This paper denonstrates how mon-montonic reasoning can be carried out using
ordinary first order systems using contexts (ie FOL contexts (note the date)
not JMCs {ref} rework of the situation calculus). It was written in responce
to the McDermott and Doyle paper {ref} where they introduced non-monotonic
logic. This was a lively discussion in the FOL group at the AI lab and was
written up by Fausto. The same tactic applies to circumscription and 'jumping
to conclusions'. This PDF has the pages in reverse order - How does this
happen!!!!.
1990
Carolyn L. Talcott, Richard W. Weyhrauch: Towards a Theory of Mechanizable
Theories: I, FOL Contexts: The Extensional View. ECAI 1990: 634-639
90ecai.ps
This paper was presented at ECAI 1990. Using the notion of context (note the
date) to organize and localize reasoning. It uses a proof of the correctness
of the 'samefringe' program as an example. This paper expresses the idea that
satisfaction preserving maps on contexts are at least as interesting as
validity preserving (e.g., traditional rules of inference) ones. Today we
would be more forceful: preoccuption with validity preservation is unhelpful;
the interesting operations from the point of reasoning systems are the
satisfaction preserving ones (like forgetting (which, by definition, is not
possible in a normal validity preserving theory)).
1991
F. Giunchiglia, A. Armando, A. Cimatti, E. Giunchiglia P. Pecchiari, L.
Serafini, A. Simpson, and P. Traverso. GETFOL Programmer Manual - GETFOL
version 1. Technical Report 91-0007, DIST - University of Genova, Genova,
Italy, 1991.
This is a reimplementation of FOL done by Fusto Giunchiglia and his group at
IRST in Trento, Italy. It was written in HGKM a programming language with
clean first order semantics, which was implemented in commoon lisp.. It had
wide circultion and I intend to make it available again.
Giunchiglia and P. Traverso. GETFOL User Manual - GETFOL version 1. Manual
9109-09, IRST, Trento, Italy, 1991. Also DIST Technical Report 91-0005, DIST,
University of Genova.
Ditto
F. Giunchiglia and R.W. Weyhrauch. FOL User Manual - FOL version 2. Manual
9109-08, IRST, Trento, Italy, 1991. Also DIST Technical Report 91-0006, DIST,
University of Genova.
Ditto
Fausto Giunchiglia, Luciano Serafini, Multilanguage First Order Theories of
Propositional Attitudes, in Third Scandinavian Conference on Artificial
Intelligence 1991, IOS Press, vol. 12, 1991, pp. 228-240 (Third Scandinavian
Conference on Artificial Intelligence 1991, Roskilde, Denmark) 1991
1992
Fausto Giunchiglia, Luciano Serafini, Multilanguage hierarchical logics (or:
how we can do without modal logics), in CNKBS`92, Proceedings of the First
Compulog Net Meeting on Knowledge Bases, 1992, pp. 44-45 (CNKBS`92,
Proceedings of the First Compulog Net Meeting on Knowledge Bases, Munich,
Germany) 1992
Fausto Giunchiglia, Luciano Serafini, Alex K. Simpson Hierarchical
Meta-Logics: Intuitions, Proof Theory and Semantics, in Meta-Programming in
Logic, 3rd International Workshop, META-92, Springer, vol. 649, 1992,
pp. 235-249 (Meta-Programming in Logic, 3rd International Workshop, META-92,
Uppsala, Sweden) 1992
1993
F. Giunchiglia. Contextual reasoning. Epistemologia, special issue on I
Linguag gi e le Macchine, XVI:345-364, 1993. Short version in Proceedings
IJCAI '93 Workshop on Using Knowledge in its Context, Chambery, France, 1993,
pp. 39-49. Also IRST-Technical Report 9211-20, IRST, Trento, Italy.
Fausto Giunchiglia, Luciano Serafini, Enrico Giunchiglia, Marcello Frixione
Non-Omniscient Belief as Context-Based Resoning, in 13th International Joint
Conference on Artificial Intelligence, Morgan Kaufmann, 1993, pp. 548-554
(13th International Joint Conference on Artificial Intelligence, Chambry,
France) 1993
1994
Richard W. Weyhrauch, Carolyn L. Talcott: The Logic of FOL Systems: Formulated
in Set Theory. Logic, Language and Computation 1994: 119-132
G. Criscuolo, Fausto Giunchiglia, Luciano Serafini A Foundation of Metalogical
Reasoning: OM Pairs (Propositional Case), 1994, Technical report/Other
Chiara Ghidini, Semantiche a Modelli Locali per Logiche MultiContestuali,
1994, Technical report
Multi-Agent Reasoning with Belief Contexts: The Approach and a Case Study, in
Intelligent Agents, ECAI-94 Workshop on Agent Theories, Architectures, and
Languages, Springer, vol. 890, 1995, pp. 71-85 (Intelligent Agents, ECAI-94
Workshop on Agent Theories, Architectures, and Languages, Amsterdam, The
Netherlands) 1994
F. Giunchiglia and L. Serafini. Multilanguage hierarchical logics (or: how
we can do without modal logics). Artificial Intelligence, 65:29-70, 1994.
Also IRST-Technical Report 9110-07, IRST, Trento, Italy.
Fausto Giunchiglia, Luciano Serafini Multilanguage Hierarchical Logics or:
How we can do Without Modal Logics in ARTIFICIAL INTELLIGENCE, Elsevier,
vol. 65, 1994, pp. 29-70.
F. Giunchiglia and A. Cimatti. HGKM User MANUAL. Getfol Version 2.4. 4 March
1994 DIST Technical Report No. 9107-05 (1991). DIST University of Genoa, Via
Opera Pia 11A, 16145 Genova, Italy.
hgkmman.pdf
1995
Alessandro Cimatti, Luciano Serafini Multi-Agent Reasoning with Belief
Contexts III: Towards the Mechanization, in IJCAI-95 Workshop on Modelling
Context in Knowledge Representation and Reasoning, 1995, pp. 35-45 (IJCAI-95
Workshop on Modelling Context in Knowledge Representation and Reasoning,
Montreal, Canada) 1995
A. Cimatti and L. Serafini. Multi-Agent Reasoning with Belief Contexts: the
Approach and a Case Study. In M. Wooldridge and N.R. Jennings, editors,
Intelligent Agents: Proceedings of 1994 Workshop on Agent Theories,
Architectures, and Languages, number 890 in Lecture Notes in Computer
Science, pages 71-85. Springer Verlag, 1995. Also IRST-Technical Report
9312-01, IRST, Trento, Italy.
Alessandro Cimatti, Luciano Serafini Multiagent Reasoning with Belief Contexts
II: Elaboration Tolerance, in First International Conference on Multiagent
Systems, MIT Press, 1995, pp. 57 - 64 (First International Conference on
Multiagent Systems, San Francisco, California) 1995
Enrico Giunchiglia, Fausto Giunchiglia, Luciano Serafini Agents as Reasoners,
Observers, or Arbitrary Believers, in First International Conference on
Multiagent Systems, MIT Press, 1995, pp. 448 (First International Conference
on Multiagent Systems, San Francisco, California) 1995
Enrico Giunchiglia, Fausto Giunchiglia, Luciano Serafini Agents as Reasoners,
Observers or Believers, in Topics in Artificial Intelligence. Proceedings of
the 4th Congresso AI*IA, Springer, vol. 992, 1995, pp. 414-425 (Topics in
Artificial Intelligence. Proceedings of the 4th Congresso AI*IA 1995
1996
Benerecetti, Alessandro Cimatti, Enrico Giunchiglia, Fausto Giunchiglia,
Luciano Serafini: Formal Specification of Beliefs in Multi-Agent Systems.
ATAL 1996: 117-130
Massimo Benerecetti, Alessandro Cimatti, Enrico Giunchiglia, Fausto
Giunchiglia, Luciano Serafini Context-Based Formal Specification of
Multi-Agent Systems, in Working Notes of the Third International Workshop on
Agent Theories, Architectures, and Languages [ATAL-96], 1996, pp. 295-307
(Working Notes of the Third International Workshop on Agent Theories,
Architectures, and Languages [ATAL-96], Budapest, Hungary) 1996
Giovanni Criscuolo, Fausto Giunchiglia, Luciano Serafini: A Foundation for
Metareasoning Part I: The Proof Theory. J. Log. Comput. 12(1): 167-208 (2002)
Giovanni Criscuolo, Fausto Giunchiglia, Luciano Serafini: A Foundation for
Metareasoning Part II: The Model Theory. J. Log. Comput. 12(3): 345-370 (2002)
1998
Richard W. Weyhrauch, Marco Cadoli, Carolyn L. Talcott: Using Abstract
Resources to Control Reasoning. Journal of Logic, Language and Information
7(1): 77-101 ((January) 1998)
Kluwer Academic Publishers Hingham, MA, USA
table of contents doi>10.1023/A:1008275403912
Alessandro Cimatti, Fausto Giunchiglia, Richard W. Weyhrauch: A Many-Sorted
Natural Deduction. Computational Intelligence 14(1): 134-149 (1998)
IRST
Date uncertain
Talcott, C. (joint work with Richard Weyhrauch, IBUKI), FOL: Towards an
architecture for buildi9ng automomous agents from build blocks of first order
logic, A powerpoint presentation made by C. Talcott at the University of
Maryland. Year uncertain
3jan-umd.ppt
Richard W. Weyhrauch Ibuki Inc., 340 Second Street - Suite 9, Los Altos,
CA 94022, U.S.A. (E-mail: rww@ibuki.com)
Marco Cadoli Dipartimento di Informatica e Sistemistica, Universit "La
Sapienza", Via Salaria 113, I-00198 Roma, Italy
(E-mail: cadoli@dis.uniroma1.it)
Carolyn L. Talcott Department of Computer Science, Stanford University,
Stanford, CA 94305, U.S.A. (E-mail: clt@cs.stanford.edu)
Papers refencing FOL
P. Blackburn, Chiara Ghidini, Roy Turner, and Fausto Giunchiglia Modeling and
Using Context - 4th International and Interdisciplinary Conference CONTEXT
2003, LNCS, Springer, vol. 2680, 2003 (4th International and Interdisciplinary
Conference Modeling and Using Context (CONTEXT 2003), Stanford, CA, USA) 23-25
June
Paolo Bouquet, Chiara Ghidini, Fausto Giunchiglia, Enrico Blanzieri Theories
and uses of context in knowledge representation and reasoning JOURNAL OF
PRAGMATICS, Elsevier, vol. 35, 2003, pp. 455 - 484
C. Ghidini, L. Serafini Distributed First Order Logic - revised semantics,
2005, Technical report/Other
P. Bouquet, F. Giunchiglia, H.F. van, L. Serafini, H. Stuckenschmidt
Contextualizing Ontologies JOURNAL OF WEB SEMANTICS, Elsevier, vol. , 2004,
pp. 325-343
Loris Bozzato, Mauro Ferrari, Alberto Trombetta Building a domain ontology
from glossaries: a general methodology, CEUR-WS.org, vol. 426, 2008 (SWAP
2008 - 5th Workshop on Semantic Web Applications and Perspectives, Roma,
Italy) da 15/12/2008 a 17/12/2008
Claudio Eccher, Marco Rospocher, Andreas Seyfang, Antonella Ferro, Silvia
Miksch Modeling clinical protocols using semantic MediaWiki: the case of the
Oncocure project, in ECAI 2008 Workshop on the Knowledge Management for
Healthcare Processes (K4HelP), University of Patras, 2008, pp. 20-24 (ECAI
2008 Workshop on the Knowledge Management for Healthcare Processes (K4HelP),
Patras, Greece) 21/07/2008
Loris Bozzato, Mauro Ferrari, Camillo Fiorentini, Guido Fiorino A decidable
constructive description logic., Springer, vol. 6341, 2010, pp. 51-63 (JELIA
2010 - 12th European Conference on Logics in Artificial Intelligence,
Helsinki, Finland) da 13/09/2010 a 15/09/2010
Marco Rospocher, Claudio Eccher, Chiara Ghidini, Rakebul Hasan, Andreas
Seyfang, Antonella Ferro, and Silvia Miksch Collaborative Encoding of Asbru
Clinical Protocols, 2010 (eHealth 2010 - 3rd International ICST Conference on
Electronic Healthcare for the 21st century, Casablanca, Morocco) 13-15
December 2010
Chiara Ghidini, Luciano Serafini Distributed First Order Logic, 2010,
Technical report/Other
* Mauro Dragoni, Celia da Costa Pereira, Andrea G.B. Tettamanzi An Ontological Representation of Documents and Queries for Information Retrieval Systems, 2010 (23rd International Conference on Industrial, Engineering & Other Applications of Applied Intelligent Systems, IEA-AIE 2010, Cordoba, Spain) 06/01/2010 - 04/01/2010
* Loris Bozzato, Mauro Ferrari Composition of Semantic Web Services in a Constructive Description Logic., Springer, vol. 6333, 2010, pp. 223 - 226 (RR2010 - Web Reasoning and Rule Systems, Bressanone/Brixen, Italy) da 22/09/2010 a 24/09/2010 download
* Martin Homola, Andrei Tamilin, Luciano Serafini Modeling Contextualized Knowledge, in Procs. of the 2nd Workshop on Context, Information and Ontologies (CIAO-2010), vol. 626, 2010 (2nd Workshop on Context, Information and Ontologies (CIAO-2010), Lisbon, Portugal) 10/11/2010 download
* Martin Homola, Luciano Sera?ni, Andrei Tamilin Modeling Contextualized Knowledge, in Procs. of the 6th Workshop on Semantic Web Applications and Perspectives (SWAP2010), 2010 (6th Workshop on Semantic Web Applications and Perspectives (SWAP2010), Brixen-Bressanone, Italy) da 09/21/2010 a 09/22/2010 download
* Mauro Dragoni, Celia da Costa Pereira, Andrea G.B. Tettamanzi Ontology-Based Document and Query Representation may Improve Information Retrieval, 2010 (5th European Starting AI Researcher Symposium, STAIRS 2010, Lisbon, Portugal) 08/16/2010 - 08/20/2010
pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XML Massimo Benerecetti, Fausto Giunchiglia, Luciano Serafini: A Model Checking Algorithm for Multiagent Systems. ATAL 1998: 163-176
12Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLMassimo Benerecetti, Fausto Giunchiglia, Luciano Serafini: Model Checking Multiagent Systems. J. Log. Comput. 8(3): 401-423 (1998)
1996
11Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLMassimo Benerecetti, Alessandro Cimatti, Enrico Giunchiglia, Fausto Giunchiglia, Luciano Serafini: Formal Specification of Beliefs in Multi-Agent Systems. ATAL 1996: 117-130
10Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLAlessandro Cimatti, Luciano Serafini: Mechanizing Multi-Agent Reasoning with Belief Contexts. FAPR 1996: 694-696
1995
9Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLEnrico Giunchiglia, Fausto Giunchiglia, Luciano Serafini: Agents as Reasoners, Observers or Believers. AI*IA 1995: 414-425
8no EE pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLEnrico Giunchiglia, Fausto Giunchiglia, Luciano Serafini: Agents as Reasoners, Observers, or Arbitrary Believers. ICMAS 1995: 448
7no EE pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLAlessandro Cimatti, Luciano Serafini: Multiagent Reasoning with Belief Contexts II: Elaboration Tolerance. ICMAS 1995: 57-64
1994
6Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLAlessandro Cimatti, Luciano Serafini: Multi-Agent Reasoning with Belief Contexts: The Approach and a Case Study. ECAI Workshop on Agent Theories, Architectures, and Languages 1994: 71-85
5Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLFausto Giunchiglia, Luciano Serafini: Multilanguage Hierarchical Logics or: How we can do Without Modal Logics. Artif. Intell. 65(1): 29-70 (1994)
1993
4no EE pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLFausto Giunchiglia, Luciano Serafini, Enrico Giunchiglia, Marcello Frixione: Non-Omniscient Belief as Context-Based Resoning. IJCAI 1993: 548-554
1992
3no EE pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLFausto Giunchiglia, Luciano Serafini: Multilanguage hierarchical logics (or: how we can do without modal logics). CNKBS 1992: 44-45
2Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLFausto Giunchiglia, Luciano Serafini, Alex K. Simpson: Hierarchical Meta-Logics: Intuitions, Proof Theory and Semantics. META 1992: 235-249
1991
1no EE pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLFausto Giunchiglia, Luciano Serafini: Mulitlanguage First Order Theories of Propositional Attitudes. SCAI 1991: 228-240
Coauthor Index
5Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLLuigia Carlucci Aiello, Mario Aiello, Richard W. Weyhrauch: Pascal in LCF: Semantics and Examples of Proof. Theor. Comput. Sci. 5(2): 135-177 (1977)
1976
4Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLLuigia Carlucci Aiello, Mario Aiello, Giuseppe Attardi, P. Cavallari, Gianfranco Prini: Formal Definition of Semantics of Generated Control Regimes. MFCS 1976: 173-179
1975
3no EE pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLMario Aiello, Richard W. Weyhrauch: Checking Proofs in the Metamathematics of First Order Logic. IJCAI 1975: 1-8
2Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XML Luigia Carlucci Aiello, Mario Aiello: Programming language semantics in a typed lambda - calculus. Lambda-Calculus and Computer Science Theory 1975: 240-251
1974
1Electronic Edition pubzone.org CiteSeerX Google scholar BibTeX bibliographical record in XMLLuigia Aiello, Mario Aiello: Proving program correctness in L. C. F.. Symposium on Programming 1974: 59-71
Luigia Carlucci Aiello, Mario Aiello, Richard W. Weyhrauch: Pascal in LCF: Semantics and Examples of Proof. Theor. Comput. Sci. 5(2): 135-177 (1977)
Jussi Ketonen, Richard W. Weyhrauch: A Decidable Fragment of Predicate Calculus. Theor. Comput. Sci. 32: 297-307 (1984)
John McCarthy. Formalizing Common Sense: Papers by John McCarthy. Ablex Publishing Corporation, 355 Chestnut Street, Norwood, NJ 07648, 1990.
John McCarthy and Patrick Hayes. Some philosophical problems from the standpoint of artificial intelligence. In B. Meltzer and D. Michie, editors, Machine Intelligence, volume 4, pages 463-502. Edinburgh University Press, Edinburgh, 1969. Reprinted in [41].
Jon Doyle. A truth maintenance system. Artificial Intelligence, 12:231-272, 1979.
R.V. Guha. Contexts: A Formalization and Some Applications. PhD thesis, Stanford University, 1991. Also technical report STAN-CS-91-1399-Thesis, and MCC Technical Report Number ACT-CYC-423-91.
John McCarthy. Notes on formalizing context. In Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence, 1993.
Semantic matching: Algorithms and implementation
by Fausto Giunchiglia, Mikalai Yatskevich, Pavel Shvaiko - JOURNAL ON DATA SEMANTICS , 2007
"... We view match as an operator that takes two graph-like structures (e.g., classifications, XML schemas) and produces a mapping between the nodes of these graphs that correspond semantically to each other. Semantic matching is based on two ideas: (i) we discover mappings by computing semantic relation ..."
@inproceedings{aiello-80lpw,
author = {Aiello, L.},
year = 1980,
title = {Evaluating functions defined in first order logic},
booktitle = { Proceedings of the Logic programming workshop},
place = {Debrecen Hungary}}
@inproceedings{aiello-80aaai,
author = {Aiello, L.},
year = 1980,
title = {Automatic generation of semantic attachments in {FOL}},
booktitle = { Proceedings of 1st {AAAI} conference on artificial intelligence},
pages = {90--92}
}
@techreport{aiello-aiello-weyhrauch-74pascal,
author = {Aiello, L. and Aiello, M. and Weyhrauch, R. W.},
year = 1974,
title = { The Semantics of Pascal in {LCF}},
institution = {Stanford Artificial Intelligence Laboratory},
number = {{ AIM-221}},
}
@techreport{aiello-weyhrauch-74pascal,
author = {Aiello, L. and Weyhrauch, R. W.},
year = 1974,
title = {{ LCFsmall}: an Implementation of {LCF}},
institution = {Stanford Artificial Intelligence Laboratory},
number = {{ AIM-241}},
}
@inproceedings{aiello-weyhrauch-75ijcai,
author = {Aiello, L. and Weyhrauch, R. W.},
year = 1975,
title = {Checking Proofs in the Metamathematics of First Order Logic},
booktitle = {Proceedings of the Fourth International Joint Conference
on Artificial Intelligence},
pages = { 1--8},
}
@inproceedings{aiello-weyhrauch-75ijcai,
author = {Aiello, L. and Weyhrauch, R. W.},
year = 1980,
title = {Using meta-theoretic reasoning to do algebra},
booktitle = {\it Proceedings of the 5-th automated deduction conference},
place = {Les Arcs France},
year = 1980,
}
@phdthesis{bulnes-??,
author = {Bulnes, J.}
title = {GOAL},
school = {Stanford University}
year = 198?,
}
@techreport{filman-weyhrauch-76primer,
author = {Filman, R. E. and Weyhrauch, R. W. },
year = 1976,
title = { An FOL Primer},
institution = {Stanford University, Computer Science Department}
number = {{ STAN--CS--76--572}},
}
@article{ketonen-weyhrauch-84tcs,
author = {Ketonen, J. and Weyhrauch, R. W.},
year = 1984,
title = {A Decidable Fragment of Predicate Calculus},
journal = {Theoretical Computer Science},
volume = 32,
pages = {297--307}
}
@inproceedings{talcott-weyhrauch-90ecai,
author={Talcott, C. L. and Weyhrauch R. W.},
year={1990},
title={Towards a Theory of Mechanized Reasoning I:
FOL contexts, an extensional view},
booktitle={European Conference on Artificial Intelligence},
}
@misc{talcott-81folisp,
author = {Talcott, C. L.},
year = 1981,
title = {FOLISP: a system for reasoning about Lisp programs},
note = {(unpublished memo)}
}
@techreport{weyhrauch77,
author={Weyhrauch, R. W.},
year={1977},
title={{A Users Manual for Fol}},
institution={Stanford University Computer Science Department},
number={STAN-CS-77-432}
}
@inproceedings{weyhrauch78,
author={Weyhrauch, R. W.},
year={1978},
title={{The uses of logic in artificial intelligence}},
booktitle={Lecture Notes prepared for the summer school on the foundations
of artificial intelligence and computer science (FAICS'78), Pisa, Italy}
}
@article{weyhrauch80,
author={Weyhrauch, R. W.},
year={1980},
title={{Prolegomena to a theory of formal reasoning}},
journal={Artificial Intelligence},
volume={13},
pages={133--170}
}
@incollection{weyhrauch-talcott-94takasu-fol,
author={Weyhrauch, R. W. and Talcott, C. L.},
title={The Logic of FOL Systems: Formulated in Set Theory},
year = 1994,
series = lncs,
number = 792,
publisher = {Springer-Verlag},
booktitle ={Festschrift in honor of Professor Satoru Takasu},
editor = {Hagiya, M. and Jones, N. D. and Sato, M.},
ftp-source = {sail.stanford.edu:pub/MT/94takasu-fol.ps.Z},
keywords = {first-order logic, FOL context, partial structure, FOL system,
representation, reasoning},
}
@misc{weyhrauch-talcott-95fset,
author={Weyhrauch, R. W. and Talcott, C. L.},
title={{The Logic of FOL Systems: A Set Theoretic View }},
year = 1995,
clt-note = {in preparation -- refinement of weyhrauch-talcott-94takasu-fol }
}
@misc{weyhrauch-talcott-95pgm,
author={Weyhrauch, R. W. and Talcott, C. L.},
title={{The Logic of FOL Systems: Formulated Using Programs }},
year = 1995,
clt-note = {in preparation}
}
@misc{talcott-weyhrauch-95csys,
author={Weyhrauch, R. W. and Talcott, C. L.},
title={{Computation Systems with Restartable Computations}},
year = 1995,
clt-note = {in preparation}
}
Byte Cover
Byte Magazine