| Autor: |
Casagrande, A., Francesco Di Cosmo, Omodeo, E. G. |
| Přispěvatelé: |
Maximiliano Cristiá, David Delahaye, Catherine Dubois, Casagrande, Alberto, DI COSMO, Francesco, Omodeo, Eugenio |
| Jazyk: |
angličtina |
| Rok vydání: |
2018 |
| Předmět: |
|
| Zdroj: |
Scopus-Elsevier |
| Popis: |
Inspired by some recent revisitations of the Cantor-Bernstein theorem, in particular its formalizations in ZF carried out via the proof assistant AProS by W. Sieg and P. Walsh, we are carrying out the proof of a related graph-theoretical proposition. Our development is assisted by the proof checker ÆtnaNova, and our proof pattern is drawn from Halmos’s classic ‘Naive set theory’. This case-study illustrates the flexibility of a proof environment rooted in Set Theory, which can be bent with equal ease toward declarative and procedural styles of proof. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
