UNB Scholar Research Repository :: Browsing by Author "Horton, J., D."

Browsing by Author "Horton, J., D."

Now showing 1 - 16 of 16

A hyperfactorization of order 8, index 2
(1988) Horton, J., D.
A lower bound on the number of one-factors in bicubic graphs
(1984) Horton, J., D.
The number of one-factors in a bicubic graph is shown to be more than polynomial in the number of vertices. Thus the permanent of a matrix of 0's and 1's in which each row and column includes precisely three 1's is more than polynomial. This improves the known lower bound of 3n. The form of the bound for a graph with 2n vertices is cnan [an superscript], where c is some constant and a < log 2[subscript] (9/4)=.85... . OTHER KEYWORDS: permanents, 0-1 matrices
A polynomial-time algorithm to find the shortest cycle basis of a graph
(1984) Horton, J., D.
Define the length of a basis of a cycle space to be the sum of the lengths of all circuits in the basis. An algorithm is given that finds a basis with the shortest length in 0(e[superscript 3]v) operations. Edges may be weighted or unweighted.
An Idea for a Project: A Universe for the Evolution of Consciousness
(2010) Horton, J., D.
To the reader. This document is mainly for myself. It is for the most part a record of some of my musings over about two weeks in November of 2007, as the ideas developed and changed. I gave a presentation to the Faculty of Computer Science on April 1, 2009, called An April Fool’s Project, after discussing the idea with a few people. Nothing here is fixed yet. Any feedback would be appreciated.
Bottom up procedures to construct each minimal clause tree once
(1997) Horton, J., D.; Spencer, Bruce
Bottom up procedures are introduced for constructing only minimal clause trees. Two general methods are proposed. The first performs surgery on each non-minimal clause tree; the second ignores non-minimal clause trees and retains only minimal ones. By ranking open leaves and activating/deactivating leaves according to the ranking, the second method constructs each minimal clause tree exactly once. Methods for incorporating subsumption are described and a prototype system for propositional logic is compared against OTTER.
Bottom-up procedures for minimal clause trees
(1996) Horton, J., D.; Spencer, Bruce
Clause trees provide a basis for reasoning procedures .that use binary resolution. In this paper binary resolution trees are used as the data structure for implementing these procedures. Several properties of these procedures are explored: size, stages, minimality, disequalities, activity and rank. Procedures for uniquely building all minimal clause trees are introduced. Ordinary subsumption within these procedures does not preserve completeness, but contracting subsumption, a new restricted form of subsumption that relates to clause trees, can be integrated. The minimal restriction and unique construction address the problem of redundancy with binary resolution.
Clause trees: a tool for understanding and implementing resolution in automated reasoning
(1995) Horton, J., D.; Spencer, Bruce
A new methodology/data structure, the clause tree, is developed for automated reasoning based on resolution in first order logic. A clause tree T on a set S of clauses is a 4-tuple , where N is a set of nodes, divided into clause nodes and atom nodes, E is a set of edges, each of which joins a clause node to an atom node, L is a labeling of NuE which assigns to each clause node a clause of S, to each atom node an instance of an atom of some clause of S, and to each edge either+ or-. An instance of a clause C in S is represented by an elementary clause tree which consists of a single clause node labeled by S and joined to atom nodes labeled by the atoms of the instance. The edge joining a clause node to an atom node is labeled by the sign of the corresponding literal in the clause. A resolution is represented by unifying two atom nodes of different clause trees which represent complementary literals. In T an atom node can be adjacent either to one clause node, or to two clause nodes if it has been resolved on. The merge of two identical literals is represented by placing the path joining the two corresponding atom nodes that are leaves of the tree into the set M of chosen merge paths. The tail of the merge path becomes a closed leaf, while the head remains an open leaf which can be resolved on. The clause cl(T) that T represents, is the set of literals corresponding to the labels of the open leaves modified by the signs of the incident edges. The fundamental purpose of a clause tree T is to show that cl(T) can be derived from S using resolution. Loveland's model elimination ME, the selected literal procedure SL, and Shostak's graph construction procedure GC are explained in a unified manner using clause trees. The condition required for choosing a merge path whose head is not a leaf is given. This allows a clause tree to be built in one way (the build time) but justified as a proof in another (the proof time). The ordered clause set restriction and the foothold score restriction are explained using the operation on clause trees of merge path reversal. A new procedure called ALPOC, which combines ideas from ME, GC and OC to form a new procedure tighter than any of the top down procedures above, is developed and shown to be sound and complete. Another operation on clause trees called surgery is defined, and used to define a minimal clause tree. Any non-minimal clause tree can be reduced to a minimal clause tree using surgery, thereby showing that non-minimal clause trees are redundant. A sound procedure MinALPOC that produces only minimal clause trees is given, but whether it is complete is not known. Mergeless clause trees are shown to be equivalent to each of linear resolution, unit resolution and relative Horn sets, thereby giving short proofs of some known results. Many other new proof procedures using clause trees are discussed briefly, leaving many open questions.
Combining Rank/Activity with Set of Support, Hyperresolution and Subsumption
Horton, J., D.; Spencer, Bruce
The rank/activity (R/A) restriction of binary resolution specifies that literals in clauses have ranks, and are either active (can be resolved) or inactive. When a literal is resolved, literals in the new clause, that were of lower rank in the parent clause than the resolved literal, become inactive in the child clause. Literals that merge or factor with literals from other clauses become active. Two derivations are equivalent if they consist of the same resolutions, possibly in a different order, but resulting in the same clause. It is known that with R/A, no two equivalent derivations are found (uniqueness), but that one derivation from each equivalence class is found. In !Jlls paper, R/A is combined with the set of support strategy, with hyperresolution, and also with subsumption. In the first two cases, both completeness and uniqueness are n;taintained. In the subsumption case, completeness and uniqueness can be retained if full rank/activity is kept, but subsumption of small clauses by bigger clauses is not done. With full subsumption, and a restricted version of R/A, completeness is kept but uniqueness is lost.
Detecting Cascade Vulnerability in Linear Time
(2000) Horton, J., D.
The cascade vulnerability detection problem asks whether an opponent can use interconnections to pass data improperly across a network of individually accredited systems without having to defeat any single system that is rated high enough to be judged safe for the particular data flow. In the most general setting, an algorithm is given of time complexity O(CD2U2 + LDU), where C is the number of computers, D is the number of different classes of data, U is the number of different classes of user, and L is the number of links in the network. In the case with a linear data classification, the time complexity reduces to O(CD2 + LD), which improves on the previous best complexity of O(C3D). The case with parallel linear data classes is also solved in O(CD2 + LD) time. Keywords: algorithm, network security, cascade vulnerability, detection problem
Experiments with the ALPOC theorem prover
(1995) Spencer, Bruce; Horton, J., D.; Francis, Kelsey
A system for selecting and preparing a batch of data files, and running a selected computer program with each data file is described. Another facility collects the experimental results from several different batches and summarizes the results in a tabular form. A theorem prover, ALPOC, is implemented that combines Shostak's C-literal resolution steps with Stickel's PTTP compiler, and uses Spencer's Ordered Clause set restriction. A series of experiments is run that compares ALPOC with PTTP, using the batch system. The results are summarized and compared with Stickel's PTTP implemented in Prolog. The results show that ALPOC is slower than PTTP by a factor of at most 4, but frequently is much faster. On the problems where ALPOC is faster the number of extension steps in the ALPOC proof is less than the PTTP proof, which leads the iterative deepening search method to explore fewer levels.
Factoring the product of a cubic graph and a triangle
(1989) Horton, J., D.
Kotzig [J. Graph Theory 3 (1979) pp 23-34] proved that for any cubic graph G and any circuit of length n, C , n>3, the (Cartesian) product GxC has a 1-factorization, and that if G contains a bridge, GxC3 does not. In this paper it is shown that if G is a 2-connected cubic graph, then GxC3 decomposes into two hamilton circuits and a 1-factor.
High Arity Nodes, Routing and Internet Tomography
Horton, J., D.; Lopez-Ortiz, A.
Internet topology information is only made available in aggregate form by standing routing protocols. Connectivity information and latency characteristics must therefore be inferred using indirect techniques. In this paper we consider measurement techniques using strategically place nodes called beacons. We show that computing the minimum number of required beacons on a network under a BGP-like routing policy is NP-complete and at best U(log n)-approximable. In the worst case at least n/4 and at most (n+1)/3 beacons are required for a network with n nodes. We then introduce some results and observations that allow us to propose a relatively small candidate set of beacons for the current Internet topology. The set proposed has properties with relevant applications for all paths routing on the public Internet as well as interesting economic settlement properties for public peering.
Reducing search with minimal clause trees
(1995) Horton, J., D.; Spencer, Bruce
The smallest and most efficient resolution based proof of a theorem is represented by a minimal clause tree, proposed by Horton and Spencer. A clause tree T is minimal if and only if it contains no legal tautology paths and no legal unchosen merge paths. A characterization of minimal clause trees is given in terms of derivations. A subsumption relationship between resolution based procedures is defined and all such procedures are shown to be subsumed by clause tree procedures. Three classes of procedures are proposed which produce only minimal clause trees. The first performs surgery on any clause tree that is produced to reduce it to a minimal clause tree. The second avoids any resolution that produces a clause tree on which surgery can be performed, but leaf to internal node paths are allowed to be chosen. The third, and most restrictive, avoids any resolution that produces a non-minimal clause tree. Keywords: theorem proving, reasoning (resolution), search.
Resolvable path designs
(1983) Horton, J., D.
A resolvable (balanced) path design, RBPD (v,k,) is the decomposition of λ copies of the complete graph on v vertices into edge-disjoint subgraphs such that each subgraph consists of v /k vertex-disjoint paths of length k-1 (k vertices). It is shown that an RBPD (v,3,λ) exists if and only if v = 9 (modulo 12/gcd(4,λ)), Moreover, the RBPD (v,3,λ) can have an automorphism of order v/3. For k > 3, it is shown that if v is large enough, then an RBPD (v,k,1) exists if and only if v = k2 (modulo 1cm(2k-2,k)). Also, it is shown that the categorical product of a k-factorable graph and a regular graph is also k-factorable. These results are stronger than two conjectures of Hell and Rosa.
Sets with no empty convex 7-gons
(1982) Horton, J., D.
Erdos has defined g(n) as the smallest integer such that any set of g(n) points in the plane, no three collinear, contains the vertex set of a convex n-gon whose interior contains no point of this set. Arbitrarily large sets containing no empty convex 7-gon are constructed, showing that g(n) does not exist for n > 7. Whether g(6) exists is unknown.
Support Ordered Resolution
Spencer, Bruce; Horton, J., D.
In a binary tree representation of a binary resolution proof, rotating some tree edge reorders two adjacent resolution steps. When rotation is not permitted to disturb factoring, and thus does not change the size of the tree, it is invertible and defines an equivalence relation on proof trees. When one resolution step is performed later than another after every sequence of such rotations, we say that resolution supports the other. For a given ordering on atoms, or on atom occurrences, a support ordered proof orders its resolution steps so that the atoms are resolved consistently with the given order without violating the support relation between nodes. Any proof, including the smallest proof tree, can be converted to a support ordered proof by rotations. For a total order, the support ordered proof is unique, up to rotation equivalence. The support ordered proof is also a rank/activity proof where atom occurrences are ranked in the given order. Procedures intermediate between ordered resolution and support ordered resolution are considered. One of these, 1-weak support ordered resolution, allows a resolution on a non-maximal literal only if it is immediately followed by both a factoring and a resolution on some greater literal. In a constrained experiment where ordered resolution solves only six of 408 TPTP problems with difficultly between 0.11 and 0.56, 1-weak support ordered resolution solves 75.

Browsing by Author "Horton, J., D."

Results Per Page

Sort Options