|
logica
Software didattico per l'apprendimento
della logica
| 1) Saetti's
Sentential Proof Checkers . Programma disponibile
gratuitamente on-line; è un applet che
affronta e fornisce verifiche per problemi
elementari di logica: funzioni di verità e dimostrazioni di
varia natura.
Proof checker applet; truth functions
applet; boolean forms & Venn diagrams for categorical propositions (dynamic html for
NS4).
Autore: John
Saetti .
Copyright ©1997 by Grossmont College.
|
| 2) Hyperproof. Programma prodotto dai vincitori della Educom Medal
nel 1997, è utilizzabile solo su Macintosh. E' uno strumento per l'apprendimento dei principi del ragionamento
analitico e della logica simbolica; pensato per
l'utilizzo in un corso iniziale di logica, cerca fra
l'altro di conservare la pluralità delle informazioni veicolate dal linguaggio comune.
Per migliorare la sua fruibilità si avvale anche di innovative tecniche di elaborazione
grafica delle informazioni e delle deduzioni.
Hyperproof is a system for learning the principles of
analytical reasoning and proof construction,
consisting of a text and a Macintosh software program.
Unlike traditional treatments of first-order logic, Hyperproof combines graphical and sentential information, presenting
a set of logical rules for integrating these different forms of information. It also
reflects the heterogeneity of information encountered in everyday reasoning.
Progettato da: Jon Barwise, professor of philosophy, mathematics, and computer science
alla Indiana University di Bloomington e John Etchemendy, professor of philosophy and symbolic systems
alla Stanford University.
Price: U.S. $31.95
Publisher: Il Center for the Study of Language and Information (CSLI) è attivo dal
1983 nel campo degli studi interdisciplinari della teoria del linguaggio,
dell'informazione e della computazione. La sua sede è presso la Stanford University.
Distribuito sul Web da Amazon.com. |
| 3) Tarski's
World (Mac or PC). Creato dagli stessi autori di Hyperproof, è un programma che
introduce allo studio della first-order logic, in generale, e della semantica di primo ordine, in particolare. Utilizza anche strumenti geometrici e forme di
gioco-valutazione. E' disponibile in due forme, da solo (e prende il nome di Tarski's
World 4.0 or Tarski "Lite") o come parte del textbook/software package The
Language of First-order Logic.
Tarski's World introduces your students to the
language of first-order logic. Using this program students quickly master
the meaning of the connectives and quantifiers, and soon become fluent in the symbolic
language at the core of modern logic. Tarski's World allows the students to build
three-dimensional worlds and to describe them in first-order logic. They evaluate the
sentences in the constructed worlds and if their evaluation is incorrect, the program
provides them with a game that leads them to understand where they went wrong. Tarski's
World is available in two ways, either alone (called Tarski's World 4.0 or Tarski
"Lite") or as part of the logic textbook/software package called The Language of
First-order Logic.
Autori: Jon
Barwise e John Etchemendy
Price: U.S. $21.95
Publisher: Center
for the Study of Language and Information (CSLI)
Distribuito sul Web da Amazon.com |
| 6) Bayes' Theorem (bayes.zip) 1.01 (c) Copyright 1992.
Un programma di calcolo ad impostazione didattica, per
DOS, che affronta in modo semplice e diretto il tema del calcolo delle probabilità, con una interessante
applicazione al problema della ricerca di soggetti
dispersi in ambienti inospitali.
This program deals with Probabilities,
Conditional Probabilities, Bayes' Theorem, and how they are used in Search and Rescue to look for a missing subject lost in a hostile environment.
Autori: John Masterson e David Lovelock del Department of Philosophy, Texas A&M
University.
Disponibilità: Freeware. |
| 7) Propositional Logic Program (jkpropc.zip). Programma
di calcolo e analisi di logica proposizionale
ad impostazione didattica, per DOS. Consente
l'uso di una pluralità di variabili (fino a 9); per ogni proposizione fornisce l' analisi
delle funzioni di verità, test di tautologia e display dell'albero logico, trasfomazione
nella Polish notation e display della Karnaugh Map.
PROPC can be used to perform a complete truth table
analysis of propositional formulas of arbitrary complexity. Up to 9
independent variables are allowed which implies tables may contain as many as 512 truth
value lines. The program can display the parse tree structure that corresponds to any
formula, and it can translate formulas from the common infix notation to Polish notation.
This program also generates and displays the Karnaugh Map that is associated with a given
formula or a given truth table which is comprised of 2, 3, or 4 variables. The program
also displays a minimal length formula that generates the same truth table as determined
by the Karnaugh Map.
Autore: John
Kennedy del Mathematics Department Santa Monica College, Santa Monica,
California.
Disponibilità: Freeware. |
| 8) Venn Diagram Program (venn.zip) 1.08 (c) Copyright
1990, 1991, 1992. Programma didattico e di calcolo, per DOS;
espone in forma diagrammatica
espressioni a tre variabili e con quattro operazioni. Contiene anche due giochi
di calcolo. This program displays Venn diagrams.
Expressions are constructed from the sets, A, B, C, S (universal set), and E (empty set),
and the four operations, U (union), ^ (intersection), - (relative complement), and '
(complement). There are two games in this program: find the number, and find the region.
The user can ask questions, using set notation, to obtain clues as to what the number or
region is. Sample expressions are provided.
Autori: John Masterson e David Lovelock del Department of Philosophy, Texas A&M
University.
Disponibilità: Freeware. |
| 9) Truth Table Maker (ttm120.arc) Version 1.20 Copyright (c)
1989. Programma di calcolo (DOS) scritto per
facilitare le esercitazioni ed i calcoli logici, genera tavole
di verità per l'algebra boolena.
"I wrote TTM to generate boolean algebra truth
tables in my digital design and electronics courses. It eliminates the
boring and sometimes tedious task of having to do it yourself by scratch. Some of the
expressions can get rather complicated and large. There are shortcuts, of course, but why
bother when this program will do it for you in the wink of an eye, right?! Then you can
reduce the expression yourself or whatever you chose to do".
Autore: Michael P. Kelly, U.S. Army
Disponibilità: Freeware. |
| 10) Truth Tables 1.01 (truth.zip ) (c) Copyright 1992. Programma
di calcolo, per DOS, genera tavole di verità per espressioni con quattro operazioni,
fino a tre variabili.
This program displays Truth Tables.
Expressions are constructed from the statements p, q, and r, and the four operations,
(or), (and), (not), (implies).
Autore: David Lovelock del Department of Mathematics University of
Arizona.
Disponibilità: Freware. |
| 11) MacLogic 3; software per Macintosh, è un ausilio per le dimostrazioni di
logica del primo ordine. La sua interessante peculiarità è di seguire la formalizzazione
della logica del primo ordine data da Gentzen con i suoi
sistemi di deduzione naturale. Fornisce quindi due modalità di
costruzione della dimostrazione: sia bottom-up che top-down. Apprezzabile anche l'approccio didattico di tipo euristico, vale a dire che
gli allievi sono stimolati a produrre strutture dimostrative e non solo a testare quelle
già possedute.
Proof assistant for various first-order logics,
using both natural deduction and sequent calculus; runs on Apple Macintosh.
Prodotto del Computational
Logic research group at St Andrews University,
Scotland UK.
Prices: Individual licenses, priced at 25 pounds
Educational
licenses, priced at 75 pounds
Industrial
licenses, priced at 150 pounds .
Per acquistare il prodotto inviare una richiesta a: Dr Roy Dyckhoff, Computer Science
Division, The University, St Andrews, Fife, KY16 9SS, Scotland. rd@dcs.st-andrews.ac.uk.
E' disponibile una versione demo
. |
| 12) MacLL. Programma per
Machintosh; supporta le dimostrazioni in
logica lineare.
Proof assistant for linear logics.
Prodotto del Computational Logic
research group at St Andrews University, Scotland
UK.
Disponibilità: Freeware. |
| 13) Jape 3.2. Programma per
MacOS (Le versioni SunOS, Solaris e Linux sono disponibili al
Bernard Sufrin's Jape site ad Oxford). E' uno strumento avanzato e interattivo per l'apprendimento ed il
controllo di dimostrazioni logiche. E' utilizzabile in
diversi contesti logici, fra cui il calcolo dei predicati (anche con
conclusioni multiple), la semantica operazionale, la teoria assiomatica degli
insiemi, equational reasoning in functional programs, Hindley-Milner
polymorphic type assignment, BAN authentication-protocol logic.
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 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. Jape has been applied to several logics,
including predicate calculus, operational semantics, Hindley-Milner type assignment,
axiomatic set theory, a functional programming logic, BAN logic and a Hoare logic of
program refinement.
Autori: Bernard Sufrin (Oxford) and Richard Bornat (QMW, London) .
Disponibilità: Freeware. |
| 14) The Carnegie Mellon
Proof Tutor Project (CPT I). Programma per la produzione a fini
didattici di dimostrazioni logiche; per ora limitato alla logica
delle proposizioni, promette di fornire in futuro una nuova versione che
affronti l'intera logica dei predicati.
The aims of the Proof Tutor Project are to provide students with a structured workbench for proof construction in formal logic that combines
intelligent strategic help with a sophisticated graphical
interface that demonstrably facilitates better proof construction skill.
If a student wants advice on how to proceed in an argument, the Tutor completes the
argument and enters into a dialogue with the student, asking strategic questions and
making suggestions -- based on its proof. The first version of the Carnegie Mellon Proof
tutor (CPT I) handles sentential logic. CPT
II, which is under development now, will handle full first order predicate logic.
Prodotto dal Philosophy
Department della Carnegie Mellon University, USA.
Disponibilità: Freeware, via Telnet (istruzioni alla home page). |
| 16) Internet
Prover Project. Sistema per la ricerca e la trasformazione di dimostrazioni.
"We are developing a system of proof-search and
proof-transformation. The system works on netscape".
Autore: Sachio
Hirokawa Computer Center, Kyushu University, JAPAN.
Disponibilità: applet gratuito on-line. |
17) Teaching
logic as a tool . Non si tratta di un software,
ma di un progetto didattico per l'apprendimento
della logica e della matematica basato sul testo: David Gries and Fred B. Schneider,
A Logical Approach to Discrete Math, Springer Verlag, 1993. Il progetto si
fonda sull'uso di una Equational
propositional logic E
Courseware; David Gries and Fred B. Schneider, have written a text: A
Logical Approach to Discrete Math (Springer Verlag, 1993), which attempts to
change how logic and discrete math is taught. For this purpose, they use an equational
logic, in which substitution of equals for equals rather than modus
ponens is the main inference rule. |
| 18) The
LogicWorks, Version 7.0. (Mac or PC) Strumento interattivo per la didattica e la verifica nei corsi introduttivi di logica. Modellato sulla struttura di Class Works.
This computerized workbook assists students in
introductory logic courses and complements classroom instruction. Students
profit from the individual tutorial program that covers all aspects of beginning logic.
The LogicWorks provides instant feedback, and students are continually challenged until
they figure out the correct answer to a problem. The exercises can be used with many logic
texts, such as those by Copi, Kahane, Hurley, Harrison, and others.
Autore: Rob Brady
Prodotto da: The
Philosophy DocumentationCenter, un'organizzazione non-profit attiva dal 1966, della Bowling Green State University.
Disponibilità: Student Package: $25.95; Instructor Package: Free
To place an order for The LogicWorks, contact Laura Charland at 800-444-2419, extension 1;
419-372-8157, or by e-mail at lechar@bgnet.bgsu.edu. |
| 19) Johan
Mårtensson's On-Line Logic Book. Si tratta di una
serie di applets interattivi ben costruiti e molto utili sul piano
didattico; molto interessante l'applet sul sillogismo.
"I have developed some interactive teaching tools
for the Internet, using JavaScript. Here is an interactive exercise
tool for learning sentence-calculus, a machine for checking the properties of Aristotelian
syllogisms, a little program demonstrating the non-transitivity of conditional inference,
and Goodman's matchbox a virtual experiment with matches (text in Swedish). Requires
Netscape Navigator 2.0. There is also a program that demonstrates what happens when Albert
goes to a party, and a program demonstrating a problematic consequence of David Lewis'
truth definition for counterfactuals".
Autore: Johan Mårtensson, Department of philosophy alla Goteborg University.
|
| 21) Bertrand.
Problem-solving per la logica del primo ordine.
Produce tavole di verità e, nel corso della risoluzione stessa, un interessante albero
delle proprie funzioni. Per Mac.
For the MacIntosh. Bertrand solves sets of first-order symbolic logic statements
(subject-identity supported) for satisfiability (consistency), validity, and equivalence.
It also checks single statements for "logical truth" and "logical
falsity," and produces truth-tables for single truth-functional statements. During
the solution process, Bertrand issues "status reports" which give the user
insight into the method by which Bertrand constructs the tree that provides a solution to
the problem.
Autore: Larry Herzberg,
PhD. expected UCLA '00.
Disponibilità: Freeware alla Bertrand
Download Page. |
| 22) The Argument Clinic.
Applet interessante e simpatico, valuta
natura e conclusività di argomentazioni in linguaggio naturale. Indirizzato a chi compie i primi passi nello studio della logica.
"Welcome to the argument clinic! We examine
arguments. We may find that the argument is as sound as a dollar (or
maybe even sounder than that!). On the other hand, it might limp along so badly that we'll
have to face facts and declare it an invalid, or perhaps more precisely, just plain old
invalid. Of course there are intermediate possibilities too. But you get the idea".
Prodotto da: Department
of Philosophy della University of Northern Colorado.
Disponibile come applet ad accesso gratuito on-line. E-mail:
tktrelo@bentley.unco.edu. |
| 23) Formal
Etichs. (Windows or DOS)
Programma didattico correlato all'omonimo testo, © Routledge 1998. E' uno strumento agile
e di facile utilizzo, ispirato dall'idea dominante che etica
e logica siano strettamente correlate e che quindi il loro apprendimento
debba procedere in parallelo. Con esercizi.
Formal ethics studies rational patterns in our ethical
thinking. It combines 'hard' logic and supposedly 'soft' ethics in order
to formulate ethical principles more clearly, to organize them into a defensible system,
and to help us think more rationally about morality.
Autore: Harry J. Gensler, S.J., Philosophy Department of John Carroll University in Cleveland.
Disponibilità: Freeware. |
| 25) Gateway to Logic.
Una serie di applets ben costruiti e non semplicemente dimostrativi, grazie alla possibilità
di effettuare calcoli avanzati. Possono risultare utili anche in un contesto didattico.
a) Client
side processing . Applet avanzato, offre calcoli in logica proposizionale
classica e in logiche a più valori.
Client side processing offers parse trees, alpha graphs (Peirce), Begriffsschrift
notation (Frege), Polish notation, truth tables, normal forms, miscellaneous
operations in classical propositional logic and in
some multi-valued logics.
b) Server
side processing . Applet per tavole di verità, test su teoremi di
logica proposizionale classica, e validità di calcoli proposizionali intuizionistici.
Server side processing offers parse trees, alpha graphs, Polish notation, truth tables,
normal forms, and a theorem prover (classical propositional logic). A new task checks for propositional intuitionistic validity.
c) Proof
builder . Permette la costruzione interattiva
di dimostrazioni di logica proposizionale in calcolo deduttivo naturale.
The proof builder allows you to interactively construct
proofs in a calculus of natural deduction (based on the calculus of
Lemmon's book ``Beginning Logic'' and Colin Allen's ``Logic Primer'', respectively). It is
currently restricted to propositional logic.
d) Proof
checker . Verifica dimostrazioni.
The proof checker checks proofs in the
calculus presented by E.J. Lemmon's book "Beginning Logic'' and Colin Allen's
"Logic Primer'' (predicate logic).
Autore: Christian
Gottschall, Austria. |
| 26) Bertie3.
(Dos e Windows)
Programma didattico per l'analisi di dimostrazioni (logica proposizionale e dei predicati)
in sistemi a deduzione naturale. Impostato
in modo interattivo e con supporti grafici.
A proof checker for natural deduction systems in sentential and predicate logic. Checks the correctness of any
proof. The program uses editable "templates", which can be generated by
mentioning a rule name, and filled in as details emerge.
Autore: Austen
Clark (Professor of Philosophy, Department of Philosophy, University of Connecticut)
1992. Published in conjunction with Merrie Bergmann, Jim Moor, and Jack Nelson, The
Logic Book, 2nd edition, McGraw-Hill, 1992.
|
| 27) Twootie.
(Dos e Windows). Esploratore didattico,
molto efficace, di alberi di verità in
logica proposizionale e dei predicati.
Checks the correctness of "truth trees" or
semantic tableaux. This program contains an inference engine which it can
use to generate answers to arbitrary problems, as well as to generate hints. It comes with
some stored problem sets and allows users to construct and store problem sets of their
own. The program can print trees (answers to test problems, for example) in an attractive
format.
Autore: Austen
Clark ( Professor of Philosophy, Department of Philosophy, University of Connecticut)
1991, 1992. Published in conjunction with Merrie Bergmann, Jim Moor, and Jack Nelson, The
Logic Book, 2nd edition, McGraw-Hill, 1990; and with Richard Jeffrey, Formal
Logic: Its Scope and Limits, 3rd edition, McGraw-Hill, 1991. |
| 28) Tableau II.
(Dos) Programma di introduzione allo
studio dei tableaux (alberi sintattici) della logica
proposizionale e della logica dei predicati del primo ordine.
For philosophy students doing a first course in logic based on propositional and first-order predicate tableaux (syntactic trees). There
are 75 exercises available within the program, ordered according to an increasing degree
of difficulty.
Written by the IBM Humanities Project at the Computing Teaching Centre;
© Oxford University 1988.
Disponibilità: Freeware. |
|
