Informazioni sul documento
- Università
- Politecnico di Milano
- Corso di laurea
- Computer Engineering
- Materia
- Algebra and Mathematical Logic
- Classificazione
- Altro materiale
- Formato originale
- Testo
- Testo ricercabile
← Indietro
Altro
Spass introduction
Altro di Algebra and Mathematical Logic per il corso di Computer Engineering presso Politecnico di Milano. Materiale proveniente dall’archivio storico Studwiz e classificato per la consultazione online.
Algebra and Mathematical LogicAltro
Informazioni sul documento
Cosa trovi in questo materiale
Altro di Algebra and Mathematical Logic per il corso di Computer Engineering presso Politecnico di Milano. Materiale proveniente dall’archivio storico Studwiz e classificato per la consultazione online.
Qualità dell’importazione: il testo è stato estratto direttamente dal documento originale.
Contenuti estratti dal documento
Passaggi rappresentativi riconosciuti nelle diverse parti del materiale. Il testo completo resta presente nella pagina per la ricerca, mentre l’anteprima compatta rende più semplice la lettura.
Pagina 1
An introduction to SPASS 1 Example 1: proof found Check the correctness of the following argument: All integers are rationals. Some real numbers are not rationals. There- fore, some real numbers are not integers. 2 Example 1 / formalization Domain of the interpretation: the set of all numbers (e.g. 𝐂). Language and interpretation. Language Interpretation 𝑍𝑥 𝑥 is an integer number 𝑄𝑥 𝑥 is a rational number 𝑅𝑥 𝑥 is a real number Formulas Sentence Formula All integers are rationals ∀𝑥(𝑍𝑥 → 𝑄𝑥) Some real numbers are not rationals ∃𝑥(𝑅𝑥 ∧ ¬𝑄𝑥) Some real numbers are not integers ∃𝑥(𝑅𝑥 ∧ ¬𝑍𝑥) Argument: ∀𝑥(𝑍𝑥 → 𝑄𝑥), ∃𝑥(𝑅𝑥 ∧ ¬𝑄𝑥) ⊢ ∃𝑥(𝑅𝑥 ∧ ¬𝑍𝑥) 3 Example 1 / encoding formulas All formulas in SPASS use functional notation: FOL SPASS ∀𝑥(𝑍𝑥 → 𝑄𝑥) forall([x], implies(Z(x), Q(x))) ∃𝑥(𝑅𝑥 ∧ ¬𝑄𝑥) exists([x], and(R(x),not(Q(x)))) ∃𝑥(𝑅𝑥 ∧ ¬𝑍𝑥) exists([x], and(R(x),not(Z(x)))) 4 Example 1 / formulas: a compendium FOL SPASS ¬ lnot(formula) ∧ and(formula, formula [,formula,...] ) ∨ or(formula, formula [,formula,...] ) → implies(formula, formula ) ↔ equiv(formula, formula ) = equal(formula, formula ) ∀ forall([variable[,variable,...]],formula) ∃ exists([variable[,variable,...]],formula)
Anteprima
Prima pagina del documento.