This directory is created automatically and some papers may be mislabeled. Only document within the CiteSeer
database are listed. The directory is intended to provide entry points
for browsing the database and is not intended to be authoritative.
Papers may not appear in all relevant categories. For example, papers
in a sub-category may not appear in higher level categories.
631 Rewrite Systems - Dershowitz, Jouannaud (1990)(Correct)
Completion
Completion has recently been put in a more abstract framework [
Bachmair-et al, 1986 ] , an approach we adopt here. As in traditional
proof theory (cf. [ Takeuti, 1987 ] ), proofs are reduc... / computation automated theorem proving program specification and br approaches to equational theorem proving. In this context completion
392 Term Rewriting Systems - Klop (1992)(Correct)
Term
Rewriting Systems play an important role in various areas, such as
abstract data type specifications, implementations of functional
programming languages and automated deduction. In this chapter ... / decidability of word problems theorem proving The aim of the present br or between R rules.Prove Theorem. Let R R be
360 Intelligence without representation - Brooks (1991)(Correct)
Artificial
intelligence research has foundered on the issue of representation.
When intelligence is approached in an incremental manner, with strict
reliance on interfacing to the real world through p... / problems symbolic algebra theorem proving and other formal systems
341 A New Method for Solving Hard Satisfiability Problems - Selman, Levesque, Mitchell (1992)(Correct)
We
introduce a greedy local search procedure called GSAT for solving
propositional satisfiability problems. Our experiments show that this
procedure can be used to solve hard, randomly generated probl... / traditionally been viewed as theorem-proving problems as model-finding br is obviously satisfiable. . theorem-proving find a formal proof in a
301 The Well-Founded Semantics for General Logic Programs - Van Gelder, Ross, Schlipf (1991)(Correct)
A
general logic program (abbreviated to "program" hereafter) is a set of
rules that have both positive and negative subgoals. It is common to
view a deductive database as a general logic program consi... / Intelligence Deduction and Theorem Proving -logic programming br operation of resolution theorem proving or the law of the
268 Logical Foundations of Object-Oriented and Frame-Based Languages - Kifer, Lausen, Wu (1990)(Correct)
We propose a novel formalism, called Frame Logic (abbr., F-logic), that accounts in a clean and
declarative fashion for most of the structural aspects of object-oriented and frame-based languages.
The... / Intelligence Deduction and theorem proving-deduction logic br logic programming mechanical theorem proving General Terms Languages
255 Pushing the Envelope: Planning, Propositional Logic, and Stochastic.. - Kautz, Selman (1996)(Correct)
Planning is a notoriously hard combinatorial search
problem. In many interesting domains, current planning
algorithms fail to scale up gracefully. By combining
a general, stochastic search algorithm a... / is not amenable to general theorem-proving techniques. The origin of br using first-order resolution theorem-proving Green failed to scale
204 Systematic Nonlinear Planning - McAllester, Rosenblitt (1991)(Correct)
This paper presents a simple, sound, complete, and
systematic algorithm for domain independent STRIPS
planning. Simplicity is achieved by starting with a
ground procedure and then applying a general, ... / were based on resolution theorem proving and inherited their lifted br the development of resolution theorem proving Robinson Lifting is
179 Logic Programming in a Fragment of Intuitionistic Linear Logic - Hodas, Miller (1994)(Correct)
When logic programming is based on the proof theory of intuitionistic logic, it is natural
to allow implications in goals and in the bodies of clauses. Attempting to prove a goal of
the form D oe G fr... / examples taken from theorem proving natural language parsing br by programs in many ways. In theorem provers they can be used to store
179 CLASSIC: A Structural Data Model for Objects - Borgida, Brachman, McGuinness.. (1989)(Correct)
classic
is a data model that encourages the description of objects not only in
terms of their relations to other known objects, but in terms of a
level of intensional structure as well. The classic la... / this problem is equivalent to theorem proving for first order logic and br out as full generalpurpose theorem proving using predicates like
179 A Logic Programming Language with Lambda-Abstraction, Function.. - Miller (1991)(Correct)
ion,
Function Variables, and Simple Unification Dale Miller Department of
Computer and Information Science University of Pennsylvania
Philadelphia, PA 19104--6389 USA Abstract: It has been argued else... / meta-programs including theorem provers and program transformers br such unification in the theorem proving system Isabelle. Pfenning and
163 Formal Methods: State of the Art and Future Directions - Clarke, Wing (1996)(Correct)
We
survey recent progress in the development of mathematical techniques
for specifying and verifying complex hardware and software systems.
Many of these techniques are capable of handling industrial-... / verification model checking theorem proving Abstract We survey br new tools such as more powerful theorem provers and model checkers than were
142 A Spatial Logic based on Regions and Connection - Randell, Cui, Cohn (1992)(Correct)
We describe an interval logic for reasoning
about space. The logic simplifies an earlier
theory developed by Randell and Cohn, and
that of Clarke upon which the former was
based. The theory suppor... / reasoned about using a direct theorem proving implementation of the theory br a Challenge for Automated Theorem Provers in proc. of CADE
133 GOLOG: A Logic Programming Language for Dynamic Domains - Levesque, Reiter, Lespérance, .. (1997)(Correct)
This
paper proposes a new logic programming language called GOLOG whose
interpreter automatically maintains an explicit representation of the
dynamic world being modeled, on the basis of user supplied... / it is also problematic for the theorem proving system as it must reason br programs using conventional theorem proving techniques as in Manna and
108 Logic Programming in the LF Logical Framework - Pfenning (1991)(Correct)
this paper we describe Elf, a meta-language intended for environments dealing
with deductive systems represented in LF.
While this paper is intended to include a full description of the Elf core langu... / applications of Elf includes theorem proving and proof transformation in br a logic program corresponds to theorem proving in a meta-logic but a
91 A Fold for All Seasons - Sheard, Fegaras (1993)(Correct)
Generic
control operators, such as fold, can be generated from algebraic type
definitions. The class of types to which these techniques are
applicable is generalized to all algebraic types definable i... / optimization and theorem proving. In addition a generic br optimization and theorem proving. For example ffl
85 A Prolog Technology Theorem Prover: Implementation by an Extended.. - Stickel (1987)(Correct)
A Prolog technology theorem prover (PTTP) is an extension of Prolog that is complete
for the full first-order predicate calculus. It differs from Prolog in its use of unification
with the occurs check... / A Prolog Technology Theorem Prover Implementation by an br Abstract A Prolog technology theorem prover PTTP is an extension of
81 The TPTP Problem Library - Christian B. Suttner, Geoff Sutcliffe (1999)(Correct)
This report provides a detailed description of the TPTP Problem Library for automated
theorem proving systems. The library is available via Internet, and forms
a common basis for development of and ex... / Problem Library for automated theorem proving systems. The library is br experimentation with automated theorem provers. This report provides
76 Local Search Strategies for Satisfiability Testing - Selman, Kautz, Cohen (1995)(Correct)
It has recently been shown that local search is surprisingly good at
finding satisfying assignments for certain classes of CNF formulas [24]. In
this paper we demonstrate that the power of local sea... / many tasks were formulated as theorem proving problems and therefore
76 Integrating Decision Procedures into Heuristic Theorem Provers: A.. - Boyer, Moore (1985)(Correct)
We discuss the problem of incorporating into a heuristic theorem prover a decision procedure for a fragment
of the logic. An obvious goal when incorporating such a procedure is to reduce the search sp... / Procedures into Heuristic Theorem Provers A Case Study of Linear br incorporating into a heuristic theorem prover a decision procedure for a
75 Construction of abstract state graphs with PVS - Graf, Saidi (1997)(Correct)
We describe in this paper a method based on abstract interpretation
which, from a theoretical point of view, is similar to the splitting methods proposed
in [DGG93, Dam96] but the weaker abstract tr... / to do this we use the Pvs theorem prover SOR and our br correct before using the Coq theorem prover GvdP HSV and on Pvs
74 Symbolic Model Checking without BDDs - Biere, Cimatti, Clarke, Zhu (1999)(Correct)
Symbolic Model Checking [3, 14] has proven to be a powerful technique for the verification of
reactive systems. BDDs [2] have traditionally been used as a symbolic representation of the system.
In thi... / verification techniques e.g. theorem proving model checking is largely
73 An Extended Calculus of Constructions - Luo (1990)(Correct)
This thesis presents and studies a unifying theory of dependent types ECC ---
Extended Calculus of Constructions. ECC integrates Coquand-Huet's (impredicative)
calculus of constructions and Martin-Lof... / is the strong normalization theorem proved by using Girard-Tait's br for pragmatic applications in theorem-proving and program specification and
70 Experimental results on the crossover point in random 3sat - Crawford, Auton (1996)(Correct)
Determining whether a propositional theory is satisfiable is a prototypical example
of an NP-complete problem. Further, a large number of problems that occur in
knowledge-representation, learning, pla... / is also the essential task of a theorem prover though there is no a-priori br a-priori reason to expect that theorem proving problems fall into any
69 Proving Properties of States in the Situation Calculus - Reiter (1993)(Correct)
In the situation calculus, it is sometimes necessary to prove that
certain properties are true in all world states accessible from the initial
state. This is the case for some forms of reasoning about... / of planning views this as a theorem proving task Green To obtain br in contrast to the standard theorem-proving account of plan synthesis
67 STeP: the Stanford Temporal Prover - Manna, Anuchitanukul.. (1994)(Correct)
We describe the Stanford Temporal Prover (STeP), a system being developed to
support the computer-aided formal verification of concurrent and reactive systems
based on temporal specifications. Unlike ... / Theorem-proving support . br invariant generation and theorem-proving support for establishing
67 HYTECH: The Next Generation - Henzinger, Ho, Wong-Toi (1995)(Correct)
We describe a new implementation of HyTech
1
, a symbolic model checker
for hybrid systems. Given a parametric description of an embedded system as a collection
of communicating automata, HyTech a... / machine-assisted theorem proving Sha model checking
65 Controlled Integration of the Cut Rule into Connection Tableau Calculi - Letz, Mayr, Goller (1994)(Correct)
In this paper techniques are developed and compared which increase the inferential power
of tableau systems for classical first-order logic. The mechanisms are formulated in the framework of
connect... / Using the framework of the theorem prover SETHEO we have implemented br folding down. Key words. Theorem proving first-order logic tableaux
61 Towards an Understanding of Hill-climbing Procedures for SAT - Gent, Walsh (1993)(Correct)
Recently several local hill-climbing procedures for propositional satisfiability
have been proposed, which are able to solve large and difficult
problems beyond the reach of conventional algorithms ... / refutational theorem proving Much of the interest in br S.A. Cook. The complexity of theorem proving procedures. In Proceedings
60 Experiments with Proof Plans for Induction - Bundy, van Harmelen, Hesketh, Smaill (1992)(Correct)
The technique of proof plans, is explained. This technique is used to guide automatic
inference in order to avoid a combinatorial explosion. Empirical research is described to test
this technique in... / this technique in the domain of theorem proving by mathematical induction. br theorems is high. Keywords Theorem proving mathematical induction
59 HiLog: A Foundation for Higher-Order Logic Programming - Chen, Kifer, Warren (1989)(Correct)
We
describe a novel logic, called HiLog, and show that it provides a more
suitable basis for logic programming than does traditional predicate
logic. HiLog has a higher-order syntax and allows arbitra... / semantics resolution theorem proving database languages br programming instead of general theorem proving with HiLog. By a logic
59 Specification Matching of Software Components - Zaremski, Wing (1995)(Correct)
ing with credit is permitted. To copy otherwise, to republish, to post on
servers, to redistribute to lists, or to use any component of this work in other works, requires prior
specific permission and... / first-order logic we rely on theorem proving to determine match and br pre-post-conditions theorem proving subtyping specification
58 Encoding Plans in Propositional Logic - Kautz, McAllester, Selman (1996)(Correct)
In recent work we showed that planning problems
can be efficiently solved by general propositional
satisfiability algorithms (Kautz and Selman
1996). A key issue in this approach is the
development of... / notionof lifting from the theorem-proving community. This new encoding br to clauses in resolution theorem proving. Theorem A lifted SAT
55 Elf: A Language for Logic Definition and Verified Metaprogramming - Pfenning (1989)(Correct)
We describe Elf, a metalanguage for proof manipulation
environments that are independent of any particular
logical system. Elf is intended for meta-programs
such as theorem provers, proof transformers... / for meta-programs such as theorem provers proof transformers or type br of logics and interactive theorem proving in LF. EFS provides a nice
53 Memory-Efficient Algorithms for the Verification of Temporal.. - Courcoubetis, Vardi, Wolper.. (1992)(Correct)
This paper addresses the problem of designing memory-efficient
algorithms for the verification of temporal properties of finite-state
programs. Both the programs and their desired temporal properties
... / verification is to use a theorem-prover for an appropriate logic. br cf. Unfortunately theorem-proving systems are semi-automated at
52 Proving Java Type Soundness - Syme (1997)(Correct)
Syntax
of JavaS primitive-type = bool --- char --- short --- int --- long ---
float --- double simple-reference-type = class-name --- interface-name
component-type = simple-reference-type --- primitiv... / before we proceed. Like all theorem provers the tool we use called br are rarely provided by the theorem proving community. Researchers will
51 BLACKBOX: A New Approach to the Application of Theorem Proving to.. - Kautz, Selman (1998)(Correct)
sentations (McCarthy and Hayes 1969)
should go hand-in-hand with the study of practical
reasoning algorithms, rather than being carried out
as a separate activity.)
ffl The use of powerful new genera... / Approach to the Application of Theorem Proving to Problem Solving Henry br early attempts to use general theorem provers to solve planning problems
50 Mechanizing Programming Logics in Higher Order Logic - Gordon (1988)(Correct)
Formal
reasoning about computer programs can be based directly on the
semantics of the programming language, or done in a special purpose
logic like Hoare logic. The advantage of the first approach is... / Verification and Automated Theorem Proving edited by G. Birtwistle br in Hoare logic to theorem proving problems called
50 Dependent Types in Practical Programming - Xi (1998)(Correct)
Programming
is a notoriously error-prone process, and a great deal of evidence in
practice has demonstrated that the use of a type system in a
programming language can effectively detect program error... / for teaching me automated theorem proving and providing me with the br a research assistant on TPS a theorem proving system based on higherorder
49 Experiments in Theorem Proving and Model Checking for Protocol.. - Havelund, Shankar (1996)(Correct)
Communication protocols pose interesting and difficult challenges for
verification technologies. The state spaces of interesting protocols are either
infinite or too large for finite-state verificatio... / Experiments in Theorem Proving and Model Checking for br checking and state exploration. Theorem proving is also not effective since
48 Applying Formal Methods to the Analysis of a Key Management Protocol - Meadows (1992)(Correct)
In this paper we develop methods for analyzing key management and authentication protocols using
techniques developed for the solutions of equations in a term rewriting system. In particular, we descr... / systems do not emphasize the theorem-proving techniques that would be br tool implementing specialized theorem-proving techniques originally
46 Towards a Completeness Result for Model Checking of Security.. - Lowe (1998)(Correct)
Gavin Lowe
Department of Mathematics and Computer Science
University of Leicester, University Road
Leicester, LE1 7RH, UK
E-mail: gavin.lowe@mcs.le.ac.uk
Abstract
Model checking approaches to the... / combine aspects of theorem proving and model checking to try to
45 Automating Recursive Type Definitions in Higher Order Logic - Melham (1988)(Correct)
The expressive power of higher order logic makes it possible to
define a wide variety of types within the logic and to prove theorems that state
the properties of these types concisely and abstractl... / Verification and Automated Theorem Proving proceedings of the br The HOL Theorem Proving System Defining New
43 On evaluating decision procedures for modal logic - Hustadt, Schmidt (1997)(Correct)
This
paper reports on empirical performance analysis of four modal theorem
provers on benchmark suites of randomly generated formulae. The theorem
provers tested are the Davis-Putnam-based procedure K... / analysis of four modal theorem provers on benchmark suites of br generated formulae. The theorem provers tested are the
42 Automatic SAT-Compilation of Planning Problems - Ernst, Millstein, Weld (1997)(Correct)
Recent work by Kautz et al. provides tantalizing
evidence that large, classical planning problems
may be efficiently solved by translating them into
propositional satisfiability problems, using stocha... / formulation of planning as theorem proving Green most br C. Green. Application of theorem proving to problem solving. In
42 Unifying SAT-based and Graph-based Planning - Kautz, Selman (1999)(Correct)
The Blackbox planning system unifies the planning
as satisfiability framework (Kautz and Selman
1992, 1996) with the plan graph approach to
STRIPS planning (Blum and Furst 1995). We show
that STRIPS p... / early attempts to use general theorem provers to solve planning problems br described as a way to make theorem-proving practical. In other work the
40 A Tableau Calculus for Minimal Model Reasoning - Niemelä (1996)(Correct)
The paper studies the automation of minimal model inference, i.e.,
determining whether a formula is true in every minimal model of the
premises. A novel tableau calculus for propositional minimal mode... / procedure is invoked the theorem-proving task might be limited in a br clauses using a model generation theorem prover MGTP which is a parallel and
40 Completeness and Consistency in Hierarchical State-Based Requirements - Heimdahl, Leveson (1996)(Correct)
This paper describes methods for automatically analyzing formal, state-based requirements
specifications for some aspects of completeness and consistency. The approach
uses a low-level functional form... / the languages used in the theorem proving approach such as process br can be addressed by using a theorem prover. Currently however the
39 Planning for Temporally Extended Goals - Bacchus, Kabanza (1997)(Correct)
this paper appears in Proceedings of AAAI '96, pp. 1215-1222.
F. Bacchus and F. Kabanza / Temporally Extended Goals 2
Yet this flexibility also poses a problem: how do we communicate to such an agen... / work has viewed planning as a theorem proving problem. In this approach br that a plan exists. Planning as theorem proving has to date suffered from
39 Solution of the Robbins Problem - McCune (1997)(Correct)
In this article we show that the three equations known as commutativity, associativity,
and the Robbins equation are a basis for the variety of Boolean algebras. The problem
was posed by Herbert Rob... / found automatically by EQP a theorem-proving program for equational logic. br was found by EQP an automated theoremproving program for equational logic.
39 Eliminating Array Bound Checking Through Dependent Types - Xi, Pfennig (1998)(Correct)
We present a type-based approach to eliminating array bound
checking and list tag checking by conservatively extending
Standard ML with a restricted form of dependent types.
This enables the programme... / also form the basis of general theorem proving and verified program
37 Deductive Composition of Astronomical Software from Subroutine.. - Stickel, Waldinger, Lowry.. (1994)(Correct)
Automated deduction techniques are being used in a system called
Amphion to derive, from graphical specifications, programs composed
from a subroutine library. The system has been applied to construct... / domain theory by an automated theorem prover SNARK. An applicative br of automated reasoning or theorem proving-are applied to the
36 Modal Logics for Qualitative Spatial Reasoning - Brandon Bennett (1996)(Correct)
Spatial reasoning is essential for many AI applications. In most existing systems the representation
is primarily numerical, so the information that can be handled is limited to precise quantitative d... / to be tackled by existing theorem proving techniques. From a br L. Catach. Tableaux A general theorem prover for modal logics. Journal of
35 Introducing OBJ - Goguen, Winkler, Meseguer.. (1993)(Correct)
This is an introduction to OBJ, describing its philosophy, its syntax, its history, and aspects of
its semantics, both logical and operational. Many examples are given, using Release 2 of OBJ3,
which ... / and allows OBJ to be used as a theorem prover. OBJ is based upon order br this is very useful for theorem proving applications. Finally OBJ
35 Simplified and Improved Resolution Lower Bounds - Beame, Pitassi (1996)(Correct)
We give simple new lower bounds on the lengths of
Resolution proofs for the pigeonhole principle and for
randomly generated formulas. For random formulas,
our bounds significantly extend the range of ... / problem of propositional theorem proving. The most well-studied and br implementations of Resolution as theorem provers although in this case the
35 Fundamentals Of Deductive Program Synthesis - Manna, Waldinger (1992)(Correct)
An
informal tutorial is presented for program synthesis, with an emphasis
on deductive methods. According to this approach, to construct a
program meeting a given specification, we prove the existence... / transformation specifications theorem proving. Abstract An informal br the deductive-tableau system a theorem-proving framework particularly
35 Equational Term Graph Rewriting - Ariola, Klop (1993)(Correct)
We present an equational framework for term graph rewriting with cycles. The usual notion of homomorphism
is phrased in terms of the notion of bisimulation, which is well-known in process algebra and ... / programming automated theorem proving and proof theory. Term
35 Forming Concepts for Fast Inference - Kautz, Selman (1992)(Correct)
Knowledge compilation speeds inference by creating tractable approximations of a knowledge
base, but this advantage is lost if the approximations are too large. We show how learning
concept generaliza... / unknown or choose to do full theorem proving with the original theory. In br S. A. Cook. The complexity of theorem-proving procedures. In Proceedings
35 Minimal Model Generation with Positive Unit Hyper-Resolution Tableaux - Bry, Yahya (1996)(Correct)
Herbrand
models for clausal theories are useful in several areas of computer
science. In most cases, however, the conventional model generation
algorithms are inappropriate because they generate non... / in Proc. of th Wokshop on Theorem Proving with Analytic Tableaux and br computer science. In automated theorem proving models can assist in making
35 Completion without Failure - Bachmair, Dershowitz (1989)(Correct)
We present an "unfailing" extension of the standard KnuthBendix
completion procedure that is guaranteed to produce a desired canonical
system, provided certain conditions are met. We prove that this... / is refutationally complete for theorem proving in equational theories. The br of the major goals in automated theorem proving. Just adding equality axioms
35 The Notion of Proof in Hardware Verification - Cohn (1989)(Correct)
Recent advances in the field of hardware verification have raised some
fresh (and some familiar) issues to do with the scope and limitations of
formal proof. In this note, some of these are conside... / attractive application area for theorem provers for several reasons. First br Order Logic a theorem-proving system derived from R.
35 A Science of Reasoning - Bundy (1991)(Correct)
This paper addresses the question of how we can understand reasoning in general and
mathematical proofs in particular. It argues the need for a high-level understanding of
proofs to complement the l... / of the science to automatic theorem proving x before summarising br reflecting on the processes of theorem proving e.g. Polya We list
34 A Prolog Technology Theorem Prover: A New Exposition and.. - Stickel (1989)(Correct)
A Prolog technology theorem prover (PTTP) is an extension of Prolog that is complete for
the full first-order predicate calculus. It differs from Prolog in its use of unification with
the occurs check... / A Prolog Technology Theorem Prover A New Exposition and br Abstract A Prolog technology theorem prover PTTP is an extension of
34 Implementing Tactics and Tacticals in a Higher-Order Logic.. - Amy Felty (1993)(Correct)
We argue that a logic programming language with a higher-order intuitionistic logic
as its foundation can be used both to naturally specify and implement tactic style
theorem provers. The language ext... / and implement tactic style theorem provers. The language extends br starting point for implementing theorem provers and proof systems that can
33 GSAT and Dynamic Backtracking - Ginsberg, McAllester (1994)(Correct)
There
has been substantial recent interest in two new families of search
techniques. One family consists of nonsystematic methods such as GSAT;
the other contains systematic approaches that use a poly... / examples include propositional theorem proving map coloring and scheduling
33 Unification in the Union of Disjoint Equational Theories: Combining.. - Baader, Schulz (1992)(Correct)
Most
of the work on the combination of unification algorithms for the union
of disjoint equational theories has been restricted to algorithms which
compute finite complete sets of unifiers. Thus the d... / an important role in automated theorem provers with built in theories br of constraint approaches to theorem proving see e.g.Bu term
31 Model checking for infinite state systems using data abstraction.. - Dingel, Filkorn (1995)(Correct)
A
method combining data abstraction, model checking and theorem proving
is presented. It provides a semi-automatic, formal framework for
proving arbitrary linear time temporal logic properties of infi... / style reasoning and theorem proving Jurgen Dingel and br model checking and theorem proving is presented. It provides a
31 An Industrial Strength Theorem Prover for a Logic Based on Common Lisp - Kaufmann, Moore (1997)(Correct)
ACL2 is a re-implemented extended version
of Boyer and Moore's Nqthm and Kaufmann's Pc-Nqthm,
intended for large scale verification projects. This paper
deals primarily with how we scaled up Nqthm's l... / An Industrial Strength Theorem Prover for a Logic Based on Common br verification automatic theorem proving computational logic
31 PROTEIN: A PROver with a Theory Extension INterface - Peter Baumgartner, Ulrich Furbach (1994)(Correct)
PROTEIN (PROver with a Theory Extension INterface) is a PTTPbased
first order theorem prover over built-in theories. Besides various standardrefinements
known for model elimination, PROTEIN also off... / is a PTTPbased first order theorem prover over built-in theories. br PROTEIN is a complete theorem prover for first order clause logic.
31 Reusing Proofs - Kolbe, Walther (1994)(Correct)
1
We develop a learning component for a theorem
prover designed for verifying statements by mathematical induction.
If the prover has found a proof, it is analyzed yielding
a so-called catch. The c... / a learning component for a theorem prover designed for verifying br component can be developed. Theorem proving by mathematical induction
31 SCOTT: A Model-Guided Theorem Prover - John Slaney (1993)(Correct)
SCOTT (Semantically Constrained Otter) is a
resolution-based automatic theorem prover for
first order logic. It is based on the high performance
prover OTTER by W. McCune and
also incorporates a m... / SCOTT A Model-Guided Theorem Prover John Slaney Automated br is a resolution-based automatic theorem prover for first order logic. It is
30 Parametric Shape Analysis via 3-Valued Logic - Sagiv, Reps, Wilhelm (1999)(Correct)
We
present a family of abstract-interpretation algorithms that are capable
of determining "shape invariants" of programs that perform destructive
updating on dynamically allocated storage. The main id... / Logic-mechanical theorem proving General Terms Algorithms
30 Equational Reasoning and Term Rewriting Systems - Plaisted (1993)(Correct)
ordering structures and computational complexity. Technical
Report CSD-TR-621, University of London, May 1990.
[Che81] P. Chew. Unique normal forms in term rewriting systems with repeated variables. I... / First-order theorem proving br reasoning in general theorem proving programs. We also touch on
30 Finding Hard Instances of the Satisfiability Problem: A Survey - Cook, Mitchell (1997)(Correct)
Finding
sets of hard instances of propositional satisfiability is of interest
for understanding the complexity of SAT, and for experimentally
evaluating SAT algorithms. In discussing this we conside... / As the dual of propositional theorem proving it is amenable to the proof br Stephen Cook. The complexity of theorem proving procedures. In Proc. rd
30 Abstraction Mechanisms for Hardware Verification - Melham (1987)(Correct)
ion Mechanisms for Hardware
Verification
Thomas F. Melham
University of Cambridge
Computer Laboratory
New Museums Site, Pembroke Street
Cambridge, CB2 3QG, England
Abstract: It is argued that techni... / even when automated theorem proving tools are used. A
30 Implicit Induction in Conditional Theories - Bouhoula, Rusinowitch (1995)(Correct)
We
propose a new procedure for proof by induction in conditional theories
where case analysis is simulated by term rewriting. This technique
reduces considerably the number of variables of a conjectur... / easy lemmas. keywords Theorem proving Term rewriting systems br the only signicant automated theorem proving system for induction.
30 An Empirical Analysis of Search in GSAT - Gent, Walsh (1993)(Correct)
We describe an extensive study of search in GSAT, an approximation
procedure for propositional satisfiability. GSAT performs greedy hillclimbing
on the number of satisfied clauses in a truth assignm... / interpretation refutational theorem proving planning This paper is
29 Model Checking Timed Automata - Yovine (1998)(Correct)
The theory of timed automata provides a formal framework
to model and to verify the correct functioning of real-time systems.
Among the different verification problems that have been investigated
wi... / verification in contrast to theorem proving which is used to mean
29 Experience with embedding hardware description languages in HOL - Boulton, Gordon, Gordon, Harrison.. (1992)(Correct)
The semantics of hardware description languages can be represented in higher order logic.
This provides a formal definition that is suitable for machine processing. Experiments are
in progress at Camb... / tools based on the HOL theorem-proving assistant. Three languages br on building semantically-based theorem-proving tools is discussed. Keyword
29 Theorem Proving with Ordering and Equality Constrained Clauses - Nieuwenhuis, Rubio (1995)(Correct)
constraint strategies and saturation
Given a signature F , below we denote by S the set of all clauses built over F , and
similarly by C the set of all constraints, and by EC the set of all equality ... / - Theorem Proving with Ordering and Equality br useful for making parts of the theorem proving process explicit leading to
29 Any ground associative-commutative theory has a finite canonical.. - Narendran, Rusinowitch (1991)(Correct)
We
show that theories presented by a set of ground equations with several
associative-commutative (AC) symbols always admit a finite canonical
system. This result is obtained through the construction ... / tool for deriving complete theorem proving strategies with built-in br derive refutationally complete theorem-proving strategies with built-in
28 Formalizing Space Shuttle Software Requirements - Crow, Di Vito (1996)(Correct)
This paper describes two case studies in which requirements
for new flight-software subsystems on NASA's
Space Shuttle were analyzed, one using standard formal
specification techniques, the other usin... / verified using standard theorem-proving techniques. By contrast br a very effective interactive theorem prover that uses decision procedures
28 Hyper Tableaux - Peter Baumgartner, Ulrich Furbach.. (1996)(Correct)
This paper introduces a variant of clausal normal form tableaux that
we call "hyper tableaux". Hyper tableaux keep many desirable features of analytic
tableaux while taking advantage of the central ... / clauses. In saturation based theorem proving the latter turned out to be br systems are high-performance theorem provers and a parallel version of
28 Constructing Specification Morphisms - Smith (1993)(Correct)
This
paper is part of a broader research program to explore a mechanizable
model of software development based on algebraic specifications and
specification morphisms. An algebraic specification (or s... / the source theory. First-order theorem-proving techniques are used to br allows us to use theorem-proving technology to construct
28 On Shostak's Decision Procedure for Combinations of Theories - Cyrluk, Lincoln, Shankar (1996)(Correct)
Decision procedures are increasingly being employed for deciding
or simplifying propositional combinations of ground equalities involving
uninterpreted function symbols, linear arithmetic, arrays, a... / feedback and comments. in theorem proving applied to program br to automatic and semi-automatic theorem provers and proof checkers has clear
28 Multivalued Logics: A Uniform Approach to Inference in Artificial.. - Ginsberg (1988)(Correct)
This paper describes a uniform formalization of much of the current work in AI on inference systems.
We show that many of these systems, including first-order theorem provers, assumption-based truth m... / systems including first-order theorem provers assumption-based truth br same general-purpose bilattice theorem prover and differ only in the choice
28 Compilation and Verification of LOTOS Specifications - Garavel, Sifakis (1990)(Correct)
This
paper presents the main features of the Caesar system, intended for
formal unknown Compilation and Verification of LOTOS Specifications
Hubert GARAVEL
VERILOG Rhone-Alpes
Centre HITELLA
46 av... / algebraic transformations and theorem proving techniques to Lotos br ffl the efficiency of existing theorem provers is not sufficient because
27 Proof Search in the Intuitionistic Sequent Calculus - Shankar (1991)(Correct)
The use of Herbrand functions (more popularly known as Skolemization) plays an important
role in classical theorem proving and logic programming. We define a notion of Herbrand
functions for the full ... / an important role in classical theorem proving and logic programming. We br effective way to do automated theorem proving since there is more
27 A Theory of Abstraction - Giunchiglia (1992)(Correct)
ion Mappings. In Proc. 10th IJCAI
conference, pages 1011--1014. International Joint Conference on Artificial Intelligence, 1987.
[Ten88] J.D. Tenenberg. Abstraction in Planning. PhD thesis, Computer S... / mappings in mechanical theorem proving. In th Conference on br . Pla D.A. Plaisted. Theorem proving with abstraction. Artificial
27 Reasoning with Models - Roni Khardon (1996)(Correct)
We develop a model-based approach to reasoning, in which the knowledge base is represented
as a set of models (satisfying assignments) rather then a logical formula, and the set of queries
is restrict... / views reasoning as a kind of theorem proving process and is based on the br with which one can perform theorem proving efficiently BL Lev
27 Extracting Text from Proof - Coscoy, Kahn, Théry (1995)(Correct)
this
paper, we will be concerned with proof assistants that construct a
proof object, i.e. a data structure that explicitly represents the
proof of facts established with the system. Proof objects are... / are popular in the automatic theorem proving community while natural br why it is popular in interactive theorem provers and the obvious candidate
27 Effective Theorem Proving for Hardware Verification - Cyrluk, Rajan, Shankar, Srivas (1994)(Correct)
The attractiveness of using theorem provers for system design
verification lies in their generality. The major practical challenge
confronting theorem proving technology is in combining this general... / Effective Theorem Proving for Hardware Verification br The attractiveness of using theorem provers for system design
27 Experience with Predicate Abstraction - Das, Dill, Park (1999)(Correct)
ion
?
Satyaki Das
1
, David L. Dill
1
, and Seungjoon Park
2
1
Computer Systems Laboratory, Stanford University, Stanford, CA 94305
2
RIACS, NASA Ames Research Center, Moffett Field, CA 94035... / provides a means for combining theorem proving and model checking br of verifying a design using a theorem prover. This technique was
27 A Calculus for and Termination of Rippling - David Basin (1996)(Correct)
Rippling is a type of rewriting developed for inductive theorem proving that uses
annotations to direct search. Rippling has many desirable properties: for example, it is highly
goal directed, usual... / developed for inductive theorem proving that uses annotations to br Induction Inductive Theorem Proving Term Rewriting. .
27 Modular Properties of Composable Term Rewriting Systems - Ohlebusch (1994)(Correct)
Reduction Systems : : : : : : : : : : : : : : : : : : : : : : : : : : : 7
2.1.1 Partial Orderings : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 11
2.2 Term Rewriting Systems : : : : : : : ... / synthesis and automated theorem proving. We refer to the surveys of br with the aid of theorem provers by means of some
27 Extracting Text from Proofs - Coscoy, Kahn, Thery (1995)(Correct)
In this paper, we propose a method for presenting formal proofs in
an intelligible form. We describe a transducer from proof objects (-terms in the
Calculus of Constructions) to pseudo natural langu... / are popular in the automatic theorem proving community while natural br it is popular in interactive theorem provers and the obvious candidate
26 Verification of a Multiplier: 64 Bits and Beyond - Kurshan, Lamport (1993)(Correct)
Verifying a 64-bit multiplier has a computational complexity
that puts it beyond the grasp of current finite-state algorithms, including
those based upon homomorphic reduction, the induction princip... / and bdd fixed-point algorithms. Theorem proving while not bound by the same br circuit and using TLP a theorem prover based on the Temporal Logic
26 Unification and Anti-Unification in the Calculus of Constructions - Pfenning (1991)(Correct)
We present algorithms for unification and antiunification
in the Calculus of Constructions, where occurrences
of free variables (the variables subject to instantiation)
are restricted to higher-order ... / as the basis for a number of theorem provers for example and br of program development and theorem proving environments have been
26 ACL2: An Industrial Strength Version of Nqthm - Kaufmann, Moore (1996)(Correct)
ACL2 is a reimplemented extended version of Boyer and Moore's
Nqthm and Kaufmann's Pc-Nqthm, intended for large scale verification
projects. However, the logic supported by ACL2 is compatible with the... / Austin TX . y The theorem prover used in this work was br of Nqthm is its lack of theorem proving power if it would quickly
26 Planning Control Rules for Reactive Agents - Kabanza, Barbeau, St-Denis (1997)(Correct)
A traditional approach for planning is to evaluate goal statements over state trajectories
modeling predicted behaviors of an agent. This paper describes a powerful extension of
this approach for hand... / generating a reactive plan with theorem proving techniques Pnueli Rosner br the entire state space. The theorem proving approach is limited by the
26 Non-monotonic Learning - Bain, Muggleton (1992)(Correct)
This paper addresses methods of specialising first-order theories within
the context of incremental learning systems. We demonstrate the shortcomings
of existing first-order incremental learning syste... / theory and applying standard theorem proving techniques. This approach br Failure NF where a modified theorem prover infers A whenever the
26 DTRE - A Semi-Automatic Transformation System - Blaine, Goldberg (1991)(Correct)
This paper describes the theoretical framework and an implemented system (Dtre) for
the specification and verified refinement of specifications using operations on abstract
data types. The system is s... / with the aid of a mechanical theorem prover. Section of this paper br for efficiency reasons the theorem proving utilized during data
26 The Muse Approach to Or-Parallel Prolog - Ali, Karlsson (1994)(Correct)
Muse (Multi-sequential Prolog engines) is a simple and efficient approach to Orparallel
execution of Prolog programs. It is based on having several sequential Prolog
engines, each with its local addre... / expert systems theorem proving br semigroup is a theorem proving program for studying the
26 Symbolic Model Checking of Infinite State Systems Using Presburger.. - Bultan, Gerber, Pugh(Correct)
Model checking is a powerful technique for analyzing large, finite-state systems. In an infinite transition system,
however, many basic properties are undecidable. In this paper we present a new symbo... / style reasoning and theorem proving. While these techniques br style reasoning and theorem proving. Proceedings of CAV' LNCS
25 Model Checking Software Systems: A Case Study - Wing, Vaziri-Farahani (1995)(Correct)
Model
checking is a proven successful technology for verifying hardware. It
works, however, on only finite state machines, and most software
systems have infinitely many states. Our approach to applyi... / Motivation Theorem Proving and Model Checking br between these two objects theorem proving and model checking. We argue
25 Simple LPO constraint solving methods - Robert Nieuwenhuis (1993)(Correct)
We present simple techniques for deciding the satisfiability of lexicographic path
ordering constraints under two different semantics: solutions built over the given
signature and solutions in extende... / Keywords Automatic theorem proving. Terminology Let F br in rewriting and ordered theorem proving methods in first-order logic.
25 Timing Verification by Successive Approximation - Yannakakis (1992)(Correct)
We present an algorithm for verifying that a model M with timing constraints satisfies a
given temporal property T . The model M is given as a parallel composition of !-automata P i , where each
aut... / typical of approaches based on theorem proving but was not possible in the
25 Analytica - A Theorem Prover for Mathematica - Clarke, Zhao (1993)(Correct)
Analytica is an automatic theorem prover for theorems in elementary analysis. The prover
is written in Mathematica language and runs in the Mathematica environment. The goal
of the project is to use a... / Analytica -A Theorem Prover for Mathematica Edmund br U.S. government. Keywords Theorem Prover Symbolic computation
24 Agent-Based Software Engineering - Mike Wooldridge (1994)(Correct)
ion
. An agent in AOP (as in DAI) is an
autonomous concurrently executing reactive
process...
Autonomy: agents execute without direct human
or other intervention, and have control over
their own sta... / mechanism e.g.goal-directed theorem proving figure out what to do br reduces to constructive theorem proving show that j is
24 Focusing Construction and Selection of Abductive Hypotheses - Leake (1993)(Correct)
Many abductive understanding systems explain
novel situations by a chaining process that is
neutral to explainer needs beyond generating
some plausible explanation for the event being
explained. This... / understanding systems standard theorem-proving chaining techniques are
24 On Formalizing Database Updates: Preliminary Report - Reiter (1992)(Correct)
We address the problem of formalizing the evolution of a database under the effect
of an arbitrary sequence of update transactions. We do so by appealing to a first order
representation language calle... / property that they appeal to theorem-proving only with respect to the br testing reduces to first order theorem proving in the initial database
24 Formal Methods and their Role in the Certification of Critical Systems - Rushby (1995)(Correct)
This report is based on one prepared as a chapter for the FAA Digital Systems
Validation Handbook (a guide to assist FAA Certification Specialists with
Advanced Technology Issues).
1
Its purpose is ... / or checked by computer see theorem proving There are many formal br q.v.must be employed. Theorem proving and proof checking. Given a
24 Rewrite Techniques for Transitive Relations - Bachmair, Ganzinger (1994)(Correct)
We propose inference systems for dealing with transitive
relations in the context of resolution-type theorem
proving. These inference mechanisms are based
on standard techniques from term rewriting an... / the context of resolution-type theorem proving. These inference mechanisms br used in rewrite-based theorem provers. A key to the practicality
23 On Proof Normalization in Linear Logic - Galmiche, Perrier (1994)(Correct)
We present a proof-theoretic foundation for automated deduction in linear logic. At first,
we systematically study the permutability properties of the inference rules in this logical
framework and exp... / or program synthesis through theorem proving. As a matter of fact br of correct programs using a theorem proving approach in constructive
23 On the Occur-check Free Prolog Programs - Apt, Pellegrini (1994)(Correct)
Machine
is used. This tag maintains information about the context in which a variable
is used. This makes possible to optimize the generated code by avoiding calls to
the occur-check routine at the co... / intelligence Deduction and theorem proving-logic programming br clause is nicely moded. Thus to prove Theorem . it suffices to prove the
23 Symbolic Analysis for Parallelizing Compilers - Haghighat (1994)(Correct)
Symbolic Domain
The objects in our abstract symbolic domain are canonical symbolic expressions. A
canonical symbolic expression is a lexicographically ordered sequence of symbolic
terms. Each symboli... / of finite differences and theorem-proving techniques based on number br number theory and theorem-proving methods. Symbolic analysis
23 Optimal Speedup of Las Vegas Algorithms - Luby, Sinclair, Zuckerman (1993)(Correct)
Let A be a Las Vegas algorithm, i.e., A is a randomized algorithm
that always produces the correct answer when it stops but whose running
time is a random variable. We consider the problem of minimizi... / the practical application to theorem proving described in In this br Wolfgang Ertel. OR-Parallel Theorem Proving with Random Competition.
23 VCR: A VDM-based software component retrieval tool - Fischer, Kievernagel, Struckmann (1994)(Correct)
We
present a tool which allows implicit VDM specifications to be used as
search keys for the retrieval of software components. A preprocessing
phase utilizes signature matching to filter promising can... / candidates and feeds them into a theorem prover. Validated obligations denote br specification matching theorem proving model searching.
23 INKA: The Next Generation - Hutter, Sengler (1996)(Correct)
The INKA system is a first-order theorem prover with induction
based on the explicit induction paradigm. Since 1986 when a
first version of the INKA system was developed there have been many
improve... / The INKA system is a first-order theorem prover with induction based on the br The INKA system is a first-order theorem prover with induction based on the
23 An Oxford Survey of Order Sorted Algebra - Goguen, Diaconescu (1994)(Correct)
this paper has actually been executed, and most of the
output is also included. In addition, we present some new results about overloaded OSA and
about Mosses's unified algebra.
We emphasize the follo... / that using sorts in automatic theorem proving can be an advantage because br can greatly speed up certain theorem proving problems OSA adds to
23 PARTHEO: A High Performance Parallel Theorem Prover - Schumann, Letz (1990)(Correct)
PARTHEO, a sound and complete or-parallel theorem prover for first order logic is
presented. The proof calculus is model elimination. PARTHEO consists of a uniform network
of sequential theorem prov... / O A High Performance Parallel Theorem Prover J. Schumann and R. Letz br a sound and complete or-parallel theorem prover for first order logic is
22 Theorems and Algorithms: An Interface between Isabelle and Maple - Ballarin, Homann, Calmet (1995)(Correct)
Solving
sophisticated mathematical problems often requires algebraic algorithms
and theorems. However, there are no environments integrating theorem
provers and computer algebra systems which consiste... / are no environments integrating theorem provers and computer algebra br approaches towards introducing theorem proving into CAS is an extension of
22 Java light is Type-Safe - Definitely - Nipkow, von Oheimb (1998)(Correct)
Java `ight is a large sequential sublanguage of Java. We
formalize its abstract syntax, type system, well-formedness
conditions, and an operational evaluation semantics. Based
on this formalization, w... / have been done formally in the theorem prover Isabelle HOL. Thus this paper br specified and verified in the theorem prover Isabelle HOL In the
22 A Logic Programming System for Non-monotonic Reasoning - Alferes, Damásio, Pereira (1995)(Correct)
The evolution of Logic Programming semantics has included the introduction of a new
explicit form of negation, beside the older implicit (or default) negation typical of Logic
Programming. The richer ... / the development of automated theorem proving which took up the promise of br to find simple and efficient theorem proving strategies Horn clause
22 Combining Symbolic Constraint Solvers on Algebraic Domains - Kirchner, Ringeissen (1994)(Correct)
ion
An atomic constraint p ? (t 1 ; : : : ; t m ) is decomposed into a
conjunction of pure atomic constraints by introducing new equations of
the form (x = ? t), where t is an alien subterm in the con... / logic programming and theorem proving the development of br For instance in first-order theorem proving free constants and function
22 Refinement Types for Logical Frameworks - Frank Pfenning (1993)(Correct)
We propose a refinement of the type theory underlying the LF logical framework by
a form of subtypes and intersection types. This refinement preserves desirable features
of LF, such as decidability of... / programming and automated theorem proving see for example Smo br Specifying and Implementing Theorem Provers in a Higher-Order Logic
22 Design Goals for ACL2 - Kaufmann, Moore (1994)(Correct)
ACL2
is a theorem proving system under development at Computational Logic,
Inc., by the authors of the Boyer-Moore system, Nqthm, and its
interactive enhancement, Pc-Nqthm, based on our perceptions of... / Abstract ACL is a theorem proving system under development at br describe the ACL logic theorem prover interface implementation
21 Logical Support for Modularisation - Diaconescu, Goguen, Stefaneas (1993)(Correct)
Modularisation is important for managing the complex structures that
arise in large theorem proving problems, and in large software and/or hardware development
projects. This paper studies some prop... / structures that arise in large theorem proving problems and in large br languages. Modularisation for theorem proving has been studied less. This
21 AC-superposition with constraints: No AC-unifiers needed - Nieuwenhuis, Rubio (1990)(Correct)
We prove the completeness of (basic) deduction strategies with constrained clauses
modulo associativity and commutativity (AC). Here each inference generates one single
conclusion with an additional e... / symbolic constraints to theorem proving were given in KKR where br and inferences during the theorem proving process defined by Bachmair
21 A Spectral Sequence For Motivic Cohomology - S. Bloch, S. Lichtenbaum(Correct)
this paper is to construct a spectral sequence from the unknown A SPECTRAL SEQUENCE FOR MOTIVIC COHOMOLOGY
S. Bloch and S. Lichtenbaum
x0. / x of the paper are devoted to proving theorem A. Finally in x we br a moving lemma . We will prove theorem A by showing the map . .
20 Learning to Reason - Khardon (1994)(Correct)
ing with credit is permitted. To copy otherwise, to republish, to post on
servers, to redistribute to lists, or to use any component of this work in other works, requires prior
specific permission and... / Intelligence Deduction and Theorem Proving-deduction An earlier version br it does not use any logic or theorem proving To summarize the new
20 Partial Evaluation of Pattern Matching in Strings - Consel, Danvy (1989)(Correct)
This
article describes how automatically specializing a fairly naive pattern
matcher by partial evaluation leads to the Knuth, Morris & Pratt
algorithm. Interestingly enough, no theorem proving is nee... / Interestingly enough no theorem proving is needed to achieve the br Nogi that it needs using a theorem prover. This note shows that
20 Five Axioms of Alpha-Conversion - Gordon, Melham (1996)(Correct)
We present five axioms of name-carrying lambda-terms identified
up to alpha-conversion---that is, up to renaming of bound variables.
We assume constructors for constants, variables, application and ... / of Alpha Conversion'in Theorem Proving in Higher Order Logics th br with binding operators within a theorem prover. The difficulty of correctly
20 Event Calculus Planning Revisited - Shanahan (1997)(Correct)
In 1969 Cordell Green presented his seminal
description of planning as theorem proving with the
situation calculus. The most pleasing feature of Green's
account was the negligible gap between high-lev... / description of planning as theorem proving with the situation calculus. br the ideal of planning via theorem proving in a modern guise. In
20 Proof Strategies in Linear Logic - Tammet (1994)(Correct)
Linear logic, introduced by J.-Y.Girard, is a refinement of classical logic
providing means for controlling the allocation of "resources". It has aroused
considerable interest both from proof theorist... / methods for automated theorem proving in propositional linear br performed with the implemented theorem provers. Key words. Automated
20 Computing Circumscription Revisited: A Reduction Algorithm - Doherty (1995)(Correct)
In recent years, a great deal of attention has been devoted to logics of "commonsense"
reasoning. Among the candidates proposed, circumscription has been perceived as an elegant
mathematical technique... / approach are a proposal for a theorem prover for circumscription by br and then applying classical theorem-proving techniques to the resulting
20 A Meta-notation for Protocol Analysis - Cervesato, Durgin, Lincoln.. (1999)(Correct)
Most formal approaches to security protocol analysis are
based on a set of assumptions commonly referred to as the
"Dolev-Yao model." In this paper, we use a multiset rewriting
formalism, based on lin... / assumptions are used in theorem proving modelchecking methods br search-based analysis and theorem-proving analysis of protocols.
20 Authorization In Distributed Systems: A New Approach - Woo, Lam (1993)(Correct)
In most existing systems, authorization is specified using some low-level system-specific
mechanisms, e.g., protection bits, capabilities and access control lists. We argue that
authorization is an in... / matrix to a full-fledged theorem proving procedure e.g.if the
20 The Use of Planning Critics in Mechanizing Inductive Proofs - Ireland (1992)(Correct)
Proof plans provide a technique for guiding the search for a proof in
the context of tactical style reasoning. We propose an extension to this
technique in which failure may be exploited in the sear... / and is used to control the theorem prover. In contrast the proof br in automated inductive theorem proving Boyer Moore has shown
19 A HOL Extension of GNY for Automatically Analyzing Cryptographic.. - Brackin (1996)(Correct)
This
paper describes a Higher Order Logic (HOL) theory formalizing an
extended version of the Gong, Needham, Yahalom (GNY) belief logic, a
theory used by software that automatically proves authenticat... / using the standard HOL theorem-proving tools thus does not depend br The collection of standard HOL theorem-proving tools is large powerful
19 Elements of Mathematical Analysis in PVS - Dutertre (1996)(Correct)
This paper presents the formalization of some elements of
mathematical analysis using the PVS verification system. Our main motivation
was to extend the existing PVS libraries and provide means of
m... / similar developments using other theorem provers. Introduction PVS is br language coupled with a theorem prover designed for efficient
19 Parametric Circuit Representation Using Inductive Boolean Functions - Gupta, Fisher (1993)(Correct)
We have developed a methodology based on symbolic manipulation of inductive
Boolean functions (IBFs) for formal verification of inductively-defined hardware. This
methodology combines the techniques... / reasoning by induction both in theorem-proving systems and br logic setting as is done in theorem-proving systems with formal logics
19 Efficient Validity Checking for Processor Verification - Robert Jones (1995)(Correct)
We describe an efficient validity checker for the quantifier-free
logic of equality with uninterpreted functions. This logic is well
suited for verifying microprocessorcontrol circuitry since it allow... / Wil Although today's theorem provers could be used in theory to br in the context of more general theorem-proving systems. Nelson and Oppen
19 Interpreting Message Flow Graphs - Ladkin, Leue (1995)(Correct)
We give a semantics for Message Flow Graphs (MFGs), which play the role for interprocess
communication that Program Dependence Graphs play for control flow in parallel processes.
MFGs have been used... / methods usually employ theorem-proving techniques which are
19 Semantic Foundations for Embedding HOL in Nuprl - Howe (1996)(Correct)
We
give a new semantics for Nuprl's constructive type theory that
justifies a useful embedding of the logic of the HOL theorem prover
inside Nuprl. The embedding gives Nuprl effective access to most... / of the logic of the HOL theorem prover inside Nuprl. The embedding br and HOL are interactive theorem proving systems with a number of
19 Integrating Logical Functions with ILF - Dahn, Gehne, Honigmann, Walther, Wolf (1995)(Correct)
This is a description of the system ILF developed at the Humboldt-University at
Berlin
1
. ILF is a system that integrates automated theorem provers, proof tactics
for interactive deductive systems ... / system that integrates automated theorem provers proof tactics for br . Integration of Automated Theorem Provers
19 Automated Proofs of Object Code for a Widely Used Microprocessor - Yu (1992)(Correct)
Computing
devices can be specified and studied mathematically. Formal
specification of computing devices has many advantages unknown 114
Automated Proofs of Object
Code For
a Widely Used Microprocesso... / Nqthm a.k.a. the Boyer-Moore Theorem Proving System. Based on this formal br . . The Theorem Prover
18 Extending the HOL theorem prover with a Computer Algebra System to.. - Harrison (1993)(Correct)
In
this paper we describe an environment for reasoning about the reals
which combines the rigour of a theorem prover with the power of a
computer algebra system. 1 Introduction Computer theorem prov... / Extending the HOL theorem prover with a Computer Algebra br which combines the rigour of a theorem prover with the power of a computer
18 Isabelle Tutorial and User's Manual - Paulson, Nipkow (1990)(Correct)
This
manual describes how to use the theorem prover Isabelle. For beginners,
it explains how to perform simple single-step proofs in the built-in
logics. These include first-order logic, a classical s... / manual describes how to use the theorem prover Isabelle. For beginners br . . Theorem proving with Isabelle
18 The propositional formula checker HeerHugo - Groote (1999)(Correct)
HeerHugo is a propositional formula checker
1
, that determines whether a given formula is satisfiable
or not. Its name comes from the dutch railway station Heerhugowaard, as it was developed
to val... / in the area of automatic theorem proving. Introduction In br experience with the first order theorem prover otter led to the
18 A Common-Sense Model Of The Enterprise - Fox, Chionglo, Fadel (1993)(Correct)
There is a paradigm shift towards a distributed and integrated enterprise.
Currently, computer systems that support enterprise functions
were created independently. This hampers enterprise integration... / level or some type of theorem proving capability as provided say br and an accompanying theorem prover perhaps Prolog questions
18 Hierarchical Model-Based Diagnosis - Mozetic (1991)(Correct)
Model-based reasoning about a system requires an explicit
representation of the system's components and
their connections. Diagnosing such a system consists
of locating those components whose abnormal... / to abstractions used in theorem proving Giunchiglia and Walsh br abstractions -used in theorem proving and planning -which
18 Problem Structure in the Presence of Perturbations - Gomes, Selman (1997)(Correct)
Recent progress on search and reasoning procedures
has been driven by experimentation on computationally
hard problem instances. Hard random problem
distributions are an important source of such in... / in the area of automated theorem proving Fujita et al. Lam et
17 A Proof of the Church-Rosser Theorem and its Representation in a.. - Pfenning (1992)(Correct)
We give a detailed, informal proof of the Church-Rosser property for the untyped -calculus and
show its representation in LF. The proof is due to Tait and Martin-Lof and is based on the
notion of para... / has wide applicability in theorem proving and logic programming Fel br theorem in the Boyer-Moore theorem prover Sha BM uses de Bruijn
17 Free Variable Tableaux for Propositional Modal Logics - Beckert (1997)(Correct)
We present a sound, complete, modular and lean labelled tableau
calculus for many propositional modal logics where the labels contain "free"
and "universal" variables. Our "lean" Prolog implementation... / technique for first-order theorem proving-both theoretically and br Traditional tableau-based theorem provers developed during the last
17 Axiomatizing Reflective Logics and Languages - Clavel, Meseguer (1996)(Correct)
The very success and breadth of reflective techniques underscores the need for a
general theory of reflection. At present what we have is a wide-ranging variety of reflective
systems, each explained i... / well as a variety of reflective theorem proving systems are placed within a br in theorem-proving
17 Ordered Binary Decision Diagrams and the Davis-Putnam Procedure - Uribe, Stickel (1994)(Correct)
We compare two prominent decision procedures for propositional
logic: Ordered Binary Decision Diagrams (obdds) and the DavisPutnam
procedure. Experimental results indicate that the Davis-Putnam
proc... / the reach of resolutionbased theorem provers while the strength of such br can be used in refutational theorem proving or to effectively enumerate