The Experts below are selected from a list of 492 Experts worldwide ranked by ideXlab platform

Alexandru I. Tomescu - One of the best experts on this subject based on the ideXlab platform.

  • USINGÆTNANOVA TO FORMALLY PROVE THAT THE DAVIS-PUTNAM SATISFIABILITY TEST IS CORRECT
    2016
    Co-Authors: Eugenio G. Omodeo, Alexandru I. Tomescu
    Abstract:

    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 algorithm through the THEORY of recur-sive functions based on a well-founded relation, and prove it to be correct. Within the same framework, and by resorting to the Zorn Lemma, we de-velop a straightforward proof of the compactness theorem. 1

  • Using aetnanova to formally prove that the Davis-Putnam satisfiability test is correct
    Università degli Studi di Catania, 2008
    Co-Authors: Eugenio G. Omodeo, Alexandru I. Tomescu
    Abstract:

    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 algorithm through the THEORY of recursive functions based on a well-founded relation, and prove it to be correct.Within the same framework, and by resorting to the Zorn Lemma, we develop a straightforward proof of the compactness theorem.

Eugenio G. Omodeo - One of the best experts on this subject based on the ideXlab platform.

  • USINGÆTNANOVA TO FORMALLY PROVE THAT THE DAVIS-PUTNAM SATISFIABILITY TEST IS CORRECT
    2016
    Co-Authors: Eugenio G. Omodeo, Alexandru I. Tomescu
    Abstract:

    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 algorithm through the THEORY of recur-sive functions based on a well-founded relation, and prove it to be correct. Within the same framework, and by resorting to the Zorn Lemma, we de-velop a straightforward proof of the compactness theorem. 1

  • Using aetnanova to formally prove that the Davis-Putnam satisfiability test is correct
    Università degli Studi di Catania, 2008
    Co-Authors: Eugenio G. Omodeo, Alexandru I. Tomescu
    Abstract:

    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 algorithm through the THEORY of recursive functions based on a well-founded relation, and prove it to be correct.Within the same framework, and by resorting to the Zorn Lemma, we develop a straightforward proof of the compactness theorem.

Tomescu Alexandru - One of the best experts on this subject based on the ideXlab platform.

  • USING ÆTNANOVA TO FORMALLY PROVE THAT THE DAVIS-PUTNAM SATISFIABILITY TEST IS CORRECT
    Dipartimento di Matematica e Informatica, 2008
    Co-Authors: Omodeo, Eugenio G., Tomescu Alexandru
    Abstract:

    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 algorithm through the THEORY of recursive functions based on a well-founded relation, and prove it to be correct.Within the same framework, and by resorting to the Zorn Lemma, we develop a straightforward proof of the compactness theorem.This paper reports on using the ÆtnaNova/Referee proof-verificationsystem to formalize issues regarding the satisfiability of CNF-formulaeof propositional logic. We specify an “archetype” version of the Davis-Putnam-Logemann-Loveland algorithm through the THEORY of recursive functions based on a well-founded relation, and prove it to be correct.Within the same framework, and by resorting to the Zorn Lemma, we develop a straightforward proof of the compactness theorem

Geng Máté - One of the best experts on this subject based on the ideXlab platform.

  • A Zorn-Lemma alkalmazásai
    2020
    Co-Authors: Geng Máté
    Abstract:

    A Zorn-Lemma jellemzően a jólrendezési tétel és a transzfinit rekurzió elkerüléséhez és ily módon a bizonyítások leegyszerűsítéséhez nagyon hasznos eszköz, nem csak az algebrában, hanem a matematika szinte minden területén

Jianxin Zhou - One of the best experts on this subject based on the ideXlab platform.

  • extension of the Zorn Lemma to general nontransitive binary relations
    Journal of Optimization Theory and Applications, 1994
    Co-Authors: Jianxin Zhou
    Abstract:

    Let ≻ be an irreflexive (strict) binary relation on a nonempty setX. Denote the completion of ≻ by ≧, i.e.,y≧x ifx≻y does not hold. An elementx * ∈X is said to be a maximal element of ≻ onX ifx * ≧x, ∀x∈X. In this paper, an extension of the Zorn Lemma to general nontrasitive binary relations (may lack antisymmetry) is established and is applied to prove existence of maximal elements for general nontrasitive (reflexive or irreflexive) binary relations on nonempty sets without assuming any topological conditions or linear structures. A necessary and sufficient condition has been also established to completely characterize the existence of maximal elements for general irreflexive nontrasitive binary relations. This is the first such result available in the literature to the best of our knowledge. Many recent known existence sults in the literature for vector optimization are shown to be special cases of our result.