1 - 10 of 10 articles
A large part of the work on automated reasoning done in the Soviet Union in the sixties and seventies was based on the inverse method proposed by Sergey Maslov. We review the basic ideas of the method in the form that stresses its connection with resolution.
A new class of non-negative integer basis algorithms for linear equations with integer coefficients is developed. Computer experiments with one of the new algorithms and comparisons with other non-negative integer basis algorithms are reported. When the total run times for collections of common...
Restrictions of the problem of finding all maximal unifiable or minimal nonunifiable subsets to those of certain sizes are shown to be NP-hard, and consequently inappropriate in general for reducing thrashing by intelligent backtracking in resolution theorem provers and logic program executions....
The programming language TPL that is presented in this paper is a complete combination of PROLOG with a temporal language (the CTL language or other temporal languages expressed in atomata). It can be used to serve or reason along paths in a directed graph (a Kripke structure) which consists of...
We present in this paper an approach for mechanically certifying the correctness of systolic algorithms and detail the correctness proof of a systolic algorithm for a dynamic programming (optimal parenthesization) problem.
This article is the ninth of a series of articles discussing various open research problems in automated reasoning. Here we focus on finding an inference rule for set theory. The problem proposed for research asks one to find a means for building in set-theoretic reasoning in a manner similar to...
Tarski's geometry, a complete first-order axiomatization of Euclidean plane geometry, is developed within the automated reasoning system OTTER. Proofs are obtained and performance statistics supplied for most of the challenge problems appearing in the literature. Few of these problems have been...
Read and print from thousands of top scholarly journals.
Continue with Facebook
Log in with Microsoft
Already have an account? Log in
Bookmark this article. You can see your Bookmarks on your DeepDyve Library.
To save an article, log in first, or sign up for a DeepDyve account if you don’t already have one.
Sign Up Log In
To subscribe to email alerts, please log in first, or sign up for a DeepDyve account if you don’t already have one.
To get new article updates from a journal on your personalized homepage, please log in first, or sign up for a DeepDyve account if you don’t already have one.