Document information
- University
- Politecnico di Milano
- Degree programme
- Computer Engineering
- Subject
- Algebra and Mathematical Logic
- Classification
- Other study material
- Original format
- Text
- Searchable text
β Back
Other
Spass introduction
University study material for Algebra and Mathematical Logic in the Computer Engineering degree programme at Politecnico di Milano. The document covers: 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
Algebra and Mathematical LogicOther
Document information
What's included in this study material
University study material for Algebra and Mathematical Logic in the Computer Engineering degree programme at Politecnico di Milano. The document covers: 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
Import quality: text was extracted directly from the original document.
Extracted content from the document
Representative passages recognised in different parts of the material. The full extracted text remains available to search, while this compact preview makes the page easier to read.
Page 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)
Preview
First page of the document.