Zobrazeno 1 - 10
of 83
pro vyhledávání: '"Eugenio G. Omodeo"'
Publikováno v:
Le Matematiche, Vol 63, Iss 1, Pp 85-105 (2008)
This paper reports on using the ÆtnaNova/Referee proof-verification system to formalize issues regarding the satisfiability of CNF-formulae of propositional logic. We specify an “archetype” version of the Davis-Putnam-Logemann-Loveland algorit
Externí odkaz:
https://doaj.org/article/ac87e99004084628b0f3c14041f25cf5
Publikováno v:
Journal of Logic and Computation. Oxford University Press
Cantone, D, Omodeo, E G & Panettiere, M 2023, ' Reconciling transparency, low Δ 0-complexity and axiomatic weakness in undecidability proofs ', Journal of Logic and Computation, vol. 33, no. 4, pp. 738-763 . https://doi.org/10.1093/logcom/exad010
Cantone, D, Omodeo, E G & Panettiere, M 2023, ' Reconciling transparency, low Δ 0-complexity and axiomatic weakness in undecidability proofs ', Journal of Logic and Computation, vol. 33, no. 4, pp. 738-763 . https://doi.org/10.1093/logcom/exad010
In a first-order theory $\varTheta $, the decision problem for a class of formulae $\varPhi $ is solvable if there is an algorithmic procedure that can assess whether or not the existential closure $\varphi ^{\exists }$ of $\varphi $ belongs to $\var
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e02d0df67a24a7eb2b8eadc9fb2c86d7
https://doi.org/10.1093/logcom/exad010
https://doi.org/10.1093/logcom/exad010
Publikováno v:
Fundamenta Informaticae. 181:37-69
We report on an investigation aimed at identifying small fragments of set theory (typically, sublanguages of Multi-Level Syllogistic) endowed with polynomial-time satisfiability decision tests, potentially useful for automated proof verification. Lea
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2e2b9334ac7f4431879eca0928a54840
https://doi.org/10.3233/fi-2021-2050
https://doi.org/10.3233/fi-2021-2050
Publikováno v:
Theoretical Computer Science. 954:113786
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::74f2d57665fa8fc6735cc25fe5f83a91
https://doi.org/10.1016/j.tcs.2023.113786
https://doi.org/10.1016/j.tcs.2023.113786
Publikováno v:
SSRN Electronic Journal.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b6461df737313a4fabc936ebe1630c5a
https://doi.org/10.2139/ssrn.4163424
https://doi.org/10.2139/ssrn.4163424
We carry on a long-standing investigation aimed at identifying fragments of set theory that are potentially useful in automated verification with proof-checkers, such as AEtnaNova , based on the set-theoretic formalism. This note provides a complete
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::90aa69ea25772cf7a11d34fb301035ac
http://hdl.handle.net/11368/2973517
http://hdl.handle.net/11368/2973517
Publikováno v:
Fundamenta Informaticae. 181:v-vi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3c88dd8842bc836190cb71f218d1d4b6
https://doi.org/10.3233/fi-2021-2048
https://doi.org/10.3233/fi-2021-2048
Publikováno v:
Outstanding Contributions to Logic ISBN: 9783319978789
This survey discusses the interplay among unquantified re- lational logics, propositional modal logics, and set theories. To set up a common ground, cross-translation methods among languages commonly used to work with relations, modalities, and sets,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::33993b526dfcf0a98d549ee8759a49cf
http://hdl.handle.net/11390/1158242
http://hdl.handle.net/11390/1158242
Publikováno v:
Outstanding Contributions to Logic ISBN: 9783319418414
Martin Davis on Computability, Computational Logic, and Mathematical Foundations
Martin Davis on Computability, Computational Logic, and Mathematical Foundations
The way in which Martin Davis conceived the first chapter of his book “Applied nonstandard analysis ” is a brilliant example of information hiding as a guiding principle for the design of widely applicable constructions and methods of proof. We d
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6ddefcc8b9801d8d4b8730910ce6c89e
http://link.springer.com/chapter/10.1007/978-3-319-41842-1_10
http://link.springer.com/chapter/10.1007/978-3-319-41842-1_10
This treatise presents an integrated perspective on the interplay of set theory and graph theory, providing an extensive selection of examples that highlight how methods from one theory can be used to better solve problems originated in the other. Fe