|
Automated Reasoning / Formal Methods Research / Miscellaneous
- Automated Reasoning at Argonne
L'Argonne National Laboratory E' uno dei pi grossi centri di ricerca dello U.S. Department of Energy, il cui budget annuale di 470 milioni di dollari. Ecco qualche ragguaglio sulle sue attivit nel campo della logica: "Our goal is to develop techniques and build practical programs to help mathematicians, logicians, scientists, engineers, and others with some of the deductive aspects of their work. Most of our work applies to problems that can be stated in the language of first-order logic with equality. Our programs have been applied to many real problems, mostly in abstract algebra and logic, and many new results have been obtained through their use". Vengono indicati anche alcuni link a siti che si occupano di automatizzazione del ragionamento.
- Automated Reasoning Project, ANU
Informazioni sullo staff di ricerca ed accesso al software da esso sviluppato, che include FINDER (Finite Domain Enumerator), MaGIC (Matrix Generator for Implication Connectives), Kripke (a theorem prover for the relevant logic LR). Curato da John Slaney. Dalla presentazione: "The Automated Reasoning Project is a department in the Research School of Information Sciences and Engineering at the Australian National University. It is a small group conducting research into pure and applied logic. Some of its research has focussed on non-classical logic, the ARP and its predecessor logic group being best known for its work on relevant logic. The other main emphasis has been on automatic theorem proving, both for classical logic and for certain non-classical systems."
- Formal Methods and Software Engineering Group
Il gruppo, appartenenente al Dept. of Computer Science (Univ. of Reading, UK), si interessa di metodi formali in generale, di multimedia e di ingegneria del software. In particolare, il Formal Method Group si occupa di "computational logic, concurrent systems, CSP, hardware compilation, industrial-scale application, logic programming, provably correct systems, real-time systems, safety-critical systems, technology transfer, the Z notation and on-line information provision", con link su ciascuno di questi argomenti. Particolarmente interessante la pagina dedicata appunto ai "formal methods", che contiene un'ottima raccolta di links a risorse (buone in particolare la sezione che rinvia a "Individual notations, methods and tools" e la pagina "Who's Who" con centinaia di URL di studiosi del campo) legate ai "metodi formali", la cui natura viene chiarita in una pagina di background Information. Bench Prevalentemente orientato in senso informatico, il sito merita di essere visitato ed esplorato attentamente.
- Formal Methods Team Home Page
Il gruppo, che lavora alla NASA, si propone i seguenti scopi: "to advance the state-of-the-art in formal methods, making it practical for use on life-critical systems developed by the aerospace industry in the United States; to orchestrate the transfer of this technology to industry through use of carefully designed demonstration projects". Esso quindi prevalentemente orientato alla programmazione ed al controllo automatico dei processi.
- Logical Frameworks
"This is a home page for logical frameworks providing pointers to further material, including a bibliography, implementations, some researchers in the area, and recent announcements and papers.A logical framework is a formal meta-language for deductive systems. The primary tasks supported in logical frameworks to varying degrees are specification of deductive systems, search for derivations within deductive systems, meta-programming of algorithms pertaining to deductive systems, proving meta-theorems about deductive systems." La pagina curata da Frank Pfenning ed include una bibliografia e puntatori a "researchers in the area", "implementations", and "recent announcements".
- Laboratory for Applied Logic
Appartiene al Department of Computer Science at Brigham Young University: "The laboratory specializes in applying mathematical methods to problems in computer dependability". Il sito curato da Paul Black.
- Mechanized Reasoning
Pagina ancora in costruzione con informazioni e link concernenti la meccanizzazione del ragionamento. L'indice comprende: What is Automated Reasoning, Existing systems, related fields/pages, archives, Research groups and projects, Discussion forums, Journals, Organizations, An annotated reading list.
- Stanford Formal Reasoning Group
Home page del gruppo di ricerca, che si interessa dell'analisi e dello sviluppo del ragionamento formale nell'intelligenza artificiale. Contiene le home pages dei ricercatori che vi afferiscono ed altre informazioni sulle loro attivit.
- Stanford Encyclopedia of Logic Technology
Dalla presentazione: "The Stanford Encyclopedia of Logic Technology is a compendium of information about logic technology. It includes theoretical material, an index to currently available technology, and a survey of applications. It includes pointers to relevant tutorials, publications, and web sites and it includes information about people, organizations, and conferences concerned with the development, deployment, and application of logic technology." Sito in fase di costruzione con molti links non ancora attivati, ma si presenta gi ricca la parte sui "Reasonings Systems" e i materiali della sezione "Educational Materials" sono buoni.
|
|
Reviews / Online Publications
- Logic Journal of the IGPL
Pubblica papers in tutte le aree della logica pura e applicata: sistemi di logica pura, proof-theory, teoria dei modelli, ricorsività, teoria dei tipi, logiche non classiche e non monotone, ragionamento numerico e probabilistico, logica e AI, fondamenti di programmazione logica, logica e computazione, logica e linguaggio e applicazioni logiche all'ingegneria. Esce sia in forma elettronica che cartacea. Per contatti: Comments and Feedbacks oppure Dov Gabbay (curatore)
|
|
Software
- Jape -- A Framework for building Proof-Calculators
Pagina introduttiva al sito ftp da dove possibile scaricare il programma Jape per MacOS (MacIntosh) e relativa documentazione. Jape cos descritto: "Jape is an interactive tool designed to help with learning, teaching and using formal reasoning. It's a kind of interpreter: it takes in descriptions of logics as systems of inference rules, and allows you (or your friends, or your students) to control the development of proofs in that logic. It has a tactic language which is used to control the display of proofs and to allow simple searches. It's very flexible: the syntax of logical formulae, the form of judgements, the rules used, the entries in menus, the effect of selection and double-clicking -- all are under the control of the person who encodes the logic.".
- The Logic Daemon
"The Logic Daemon is a program that checks proofs via the world wide web for the logic system described in Logic Primer by Colin Allen and Michael Hand (MIT Press 1992)".
|
