1 - 7 of 7 articles
This is an expository introduction to an approach to theorem proving in higher-order logic based on establishing appropriate connections between subformulas of an expanded form of the theorem to be proved. Expansion trees and expansion proofs play key roles.
Explicit representation of negative information in logic programs is not feasible in many applications such as deductive databases and artificial intelligence. Defining default rules which allow implicit inference of negated facts from positive information encoded in a logic program has been an...
A language of equational programs together with an inference system, based on paramodulation is defined. The semantics of the language is given with respect to least models, least fixpoints and success sets and its soundness and completeness is proven using fixpoint theory. The necessity of the...
Necessary and sufficient conditions for the problem of maximizing or minimizing a function subject to inequality constraints are given by a set of equalities and inequalities known as the Kuhn-Tucker conditions. These conditions can provide an analytic solution to the optimization problem if the...
Isabelle [28, 30] is an interactive theorem prover that supports a variety of logics. It represents rules as propositions (not as functions) and builds proofs by combining rules. These operations constitute a meta-logic (or ‘logical framework’) in which the object-logics are formalized. Isabelle...
This article is the eleventh of a series of articles discussing various open research problems in automated reasoning. Here we focus on finding criteria for guaranteeing the existence of a complete set of reductions. We include a suggestion for evaluating a proposed solution to this research...
This paper presents a general approach to solve a constraint satisfaction problem over a finite domain by reducing it to unification in finite algebras. The lion and unicorn puzzle is considered as a constraint satisfaction problem and its implementation in an extended PROLOG is described.
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.