On an unsatisfiability-satisfiability prover (Q1264000)

From MaRDI portal
scientific article
Language Label Description Also known as
English
On an unsatisfiability-satisfiability prover
scientific article

    Statements

    On an unsatisfiability-satisfiability prover (English)
    0 references
    0 references
    1989
    0 references
    Summary: We study a new unsatisfiability-satisfiability prover and its basic properties. Our main results, besides the presentation of our prover, is to show that our procedure always terminates if a given set of clauses is satisfiable in some finite domain. The unsatisfiability checking of our procedure is as strong as the existing complete proof procedures, so we examine the strength of the satisfiability checking part of our procedure. We give an unsatisfiability-satisfiability prover, and show its soundness that is for any unsatisfiable set of clauses the procedure says that it is unsatisfiable, and if the procedure says that the set of clauses is satisfiable, then it is in fact satisfiable. We show that for a given set of clauses assumed to be satisfiable in a simple theory of Herbrand universe, the procedure terminates saying it is satisfiable. We show that for a given set of clauses assumed to be satisfiable in some finite domain, the procedure terminates saying it is satisfiable.
    0 references
    automated theorem proving
    0 references
    Herbrand universe
    0 references
    finite domain
    0 references

    Identifiers