Home Top: Theory: Theorem Proving [Computational Complexity Formal Languages Logic Quantum Computing Theorem Proving] |

Change ordering:

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

178 Formal Verification for Fault-Tolerant Architectures: Prolegomena to.. - Owre, Rushby, Shankar, von Henke (1995) (Correct)

PVS is the most recent in a series of verification systems developed at SRI. Its design was strongly influenced, and later refined, by our experiences in developing formal specifications and mechanica... / hardware verification theorem proving verification systems PVS. br present in Ehdm. The PVS theorem prover includes similar decision

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

104 Recursive Functions of Symbolic Expressions and Their Computation by.. - McCarthy (1960) (Correct)

this paper in L unknown Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I John McCarthy, Massachusetts Institute of Technology, Cambridge, Mass. April 1960 1 / to the problem of mechanical theorem proving. Functions and Function

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

72 Two Theses of Knowledge Representation - Language Restrictions, . . . - Doyle, Patil (1991) (Correct)

Levesque and Brachman argue that in order to provide timely and correct responses in the most critical applications, general purpose knowledge representation systems should restrict their languages by... / systems are like theorem-proving programs where telling the

72 Requirements Specification for Process-Control Systems - Leveson, Heimdahl, al. (1984) (Correct)

This paper describes an approach to writing requirements specifications for processcontrol systems, a specification language that supports this approach, and an example application of the approach and... / on traditional methods of theorem proving to analyze their models. Our

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

64 User Guide for the PVS Specification and Verification System (Beta.. - Owre And Shankar (1993) (Correct)

this document to refer to either the context or to the associated directory. Note that the directory may contain files other than those produced by or for PVS, but these are not considered to be a par... / not algorithmically decidable theorem proving may be required to establish

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

54 Constraint Programming and Database Query Languages - Kanellakis, Goldin (1994) (Correct)

The declarative programming paradigms used in constraint languages can lead to powerful extensions of Codd's relational data model. The development of constraint database query languages from logica... / and inherently exponential theorem proving Example .

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 An Algorithm for Exact Bounds on the Time Separation of Events in.. - Hulgaard, Burns, Amon, Borriello (1993) (Correct)

Determining the time separation of events is a fundamental problem in the analysis, synthesis, and optimization of concurrent systems. Applications range from logic optimization of asynchronous digita... / techniques e.g. and theorem proving e.g. For this

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 A probabilistic poly-time framework for protocol analysis - Lincoln, Mitchell, Mitchell, Scedrov (1998) (Correct)

We develop a framework for analyzing security protocols in which protocol adversaries may be arbitrary probabilistic polynomial-time processes. In this framework, protocols are written in a form of pr... / protocol analysis and theorem proving and model-checking

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 Getting to Know Each Other - Artificial Social Intelligence for.. - Dautenhahn (1995) (Correct)

This paper proposes a research direction to study the development of `artificial social intelligence' of autonomous robots which should result in `individualized robot societies'. The approach is high... / e.g. logic automated theorem proving or diagnostic reasoning In

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 System Description: Twelf -- A Meta-Logical Framework for Deductive.. - Frank Pfenning, Carsten Schürmann (1999) (Correct)

Twelf is a meta-logical framework for the specification, implementation, and meta-theory of deductive systems from the theory of programming languages and logics. It relies on the LF type theory and... / an experimental automatic meta-theorem proving component based on the br we consider the meta-theorem prover to be in a preliminary

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 VERSA: A Tool for the Specification and Analysis of Resource-Bound.. - Clarke, Lee, Xie (1995) (Correct)

VERSA is a tool that assists in the algebraic analysis of real-time systems. It is based on ACSR, a timed process algebra designed to express resource-bound real-time distributed systems. VERSA suppor... / of algebraic manipulations and theorem proving techniques. However PAM

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 Embracing Occlusion in Specifying the Indirect Effects of Actions - Gustafsson, Doherty (1996) (Correct)

In this paper, we extend PMON, a logic for reasoning about action and change, with causal rules which are used to specify the indirect effects of actions. The extension, called PMON(RCs), has the adva... / which insures that standard theorem proving techniques and their

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 Patterns in Property Specifications for Finite-State Verification - Dwyer, al. (1999) (Correct)

Model checkers and other nite-state verication tools allow developers to detect certain kinds of errors automatically. Nevertheless, the transition of this technology from research to practice has b... / In contrast to mechanical theorem proving which often requires

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 Design And Implementation Of Rock Roll: A Deductive Object-Oriented.. - Barja, Fernandes, Paton, Williams.. (1995) (Correct)

This paper presents an approach to the development of a deductive object-oriented database system, describing the key design decisions and their consequences for implementation. The approach is novel,... / Also the feasibility of a theorem-proving approach is reduced because

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 Formal Refinement Patterns for Goal-Driven Requirements Elaboration - Darimont, van Lamsweerde (1996) (Correct)

Requirements engineering is concerned with the identification of high-level goals to be achieved by the system envisioned, the refinement of such goals, the operationalization of goals into services... / can be derived using theorem proving techniques Jon Pot

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 Property Specification Patterns for Finite-State Verification - Matthew Dwyer (1998) (Correct)

Finite-state verification (e.g., model checking) provides a powerful means to detect errors that are often subtle and difficult to reproduce. Nevertheless, the transition of this technology from resea... / In contrast to mechanical theorem proving which often requires

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

17 Towards Constraint Satisfaction through Logic Programs and the Stable .. - Simons (1997) (Correct)

Logic programs with the stable model semantics can be thought of as a new paradigm for constraint satisfaction, where the rules of a program are seen as constraints on the stable models. In this work ... / reasoning automatic theorem proving. Printing Libella

CiteSeer - citeseer.org - Terms of Service - Privacy Policy - Copyright © 1997-2002 NEC Research Institute