Browsing by Author "Horton, Joseph, D."

Now showing 1 - 4 of 4
  • Thumbnail Image
    Item
    A Polynomial Time Algorithm to Find the Minimal Cycle Basis of a Regular Matroid
    (2001) Golynski, Alexander; Horton, Joseph, D.
  • Thumbnail Image
    Item
    Ancestor Reduction in Binary Resolution Trees
    Spencer, Bruce; Horton, Joseph, D.
    It is shown how the operation of ancestor reduction, found in tableaux calculi, can be applied to the resolution calculus. An efficient algorithm tells how to reorder some of the previous resolution steps in a binary resolution tree, and thus enables an additional factoring step that removes a literal from a clause. This ancestor reduction operation has a small search space, constrained by the size of the proof tree. If the additional search is successful, the new operation can eliminate literals and reduce the overall time to find a proof. A calculus is defined combining atom (literal) ordered resolution and ancestor reduction. Atom ordered resolution restricts search, but may generate large proofs for some atom orderings. This proposed theorem prover is slightly less restrictive in that an additional search for some ancestor reductions is required, but it generates smaller proof trees under many atom orderings.
  • Thumbnail Image
    Item
    Counting the number of equivalent binary resolution proofs
    Horton, Joseph, D.
    A binary resolution proof is represented by a binary resolution tree (brt) with clauses at the nodes and resolutions being performed at the internal nodes. A rotation in a brt can be performed on two adjacent internal nodes if the result of reversing the order of the resolutions does not affect the clause recorded at the node closer to the root. Two brt's are said to be rotationally equivalent if one can be obtained from the other by a sequence of rotations. Let c(T) be the number of brt's rotationally equivalent to T. It is shown that if T has n resolutions, all on distinct atoms, and m merges or factors between literals, then c(T) > 22n-O(m log(n)). Moreover c(T) can be as large as n! / (m + 1). A dynamic programming polynomial-time algorithm is also given to calculate c(T) if T has no merges or factors.
  • Thumbnail Image
    Item
    On the realizability of cardinality constraints in conceptual data models
    (1999) McAllister, Andrew, J.; Horton, Joseph, D.
    A new property of conceptual data models is introduced. Realizability extends strong satisfiability as defined by Lenzerini and Nobili, which is held by a data model when it must be possible to create at least one non-empty database in which no cardinality constraints are violated. A constraint is realizable when at least one database can be created in which the number of associations involving a specific entity instance is equal to the limit imposed by the constraint. When all constraints in a data model are realizable, then the entire model is said to be realizable. It is possible for a data model to be strongly satisfiable but not realizable, which means the latter is a more stringent test for model correctness. We define bounds imposed by cardinality constraints on the relative sizes of entity sets. A data model is shown to be realizable if and only if the bounds for any cycle of relationships are either both equal to one, or the lower bound is strictly less than one while the upper bound is strictly greater than one.