Computational metatheory in Nuprl (English)
National licence
- New search for: Howe, Douglas J.
- New search for: Howe, Douglas J.
In:
9th International Conference on Automated Deduction
;
238-257
;
1988
- Article/Chapter (Book) / Electronic Resource
-
Title:Computational metatheory in Nuprl
-
Contributors:Howe, Douglas J. ( author )
-
Published in:Lecture Notes in Computer Science ; 310 ; 238-257
-
Publisher:
- New search for: Springer Berlin Heidelberg
-
Place of publication:Berlin, Heidelberg
-
Publication date:1988-01-01
-
Size:20 pages
-
ISBN:
-
ISSN:
-
DOI:
-
Type of media:Article/Chapter (Book)
-
Type of material:Electronic Resource
-
Language:English
-
Keywords:
-
Source:
Table of contents eBook
The tables of contents are generated automatically and are based on the data records of the individual contributions available in the index of the TIB portal. The display of the Tables of Contents may therefore be incomplete.
- 1
-
First-order theorem proving using conditional rewrite rulesZhang, Hantao / Kapur, Deepak et al. | 1988
- 21
-
Elements of Z-module reasoningWang, Tie Cheng et al. | 1988
- 41
-
Learning and applying generalised solutions using higher order resolutionDonat, M. R. / Wallen, L. A. et al. | 1988
- 61
-
Specifying theorem provers in a higher-order logic programming languageFelty, Amy / Miller, Dale et al. | 1988
- 81
-
Query processing in quantitative logic programmingSubrahmanian, V. S. et al. | 1988
- 101
-
An environment for automated reasoning about partial functionsBasin, David A. et al. | 1988
- 111
-
The use of explicit plans to guide inductive proofsBundy, Alan et al. | 1988
- 121
-
Logicalc: An environment for interactive proof developmentDuchier, D. / McDermott, D. et al. | 1988
- 131
-
Implementing verification strategies in the KIV-systemHeisel, M. / Reif, W. / Stephan, W. et al. | 1988
- 141
-
Checking natural language proofsSimon, Donald et al. | 1988
- 151
-
Consistency of rule-based expert systemsBezem, Marc et al. | 1988
- 162
-
A mechanizable induction principle for equational specificationsZhang, Hantao / Kapur, Deepak / Krishnamoorthy, Mukkai S. et al. | 1988
- 182
-
Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial timeGallier, Jean / Narendran, Paliath / Plaisted, David / Raatz, Stan / Snyder, Wayne et al. | 1988
- 197
-
Towards efficient "knowledge-based" automated theorem proving for non-standard logicsMcRobbie, Michael A. / Meyer, Robert K. / Thistlewaite, Paul B. et al. | 1988
- 218
-
Propositional temporal interval logic is PSPACE completeAaby, A. A. / Narayana, K. T. et al. | 1988
- 238
-
Computational metatheory in NuprlHowe, Douglas J. et al. | 1988
- 258
-
Type inference in PrologAzzoune, H. et al. | 1988
- 278
-
Procedural interpretation of non-horn logic programsMinker, Jack / Rajasekar, Arcot et al. | 1988
- 294
-
Recursive query answering with non-horn clausesChi, Shan / Henschen, Lawrence J. et al. | 1988
- 313
-
Case inference in resolution-based languagesWakayama, T. / Payne, T. H. et al. | 1988
- 323
-
Notes on Prolog program transformations, Prolog style, and efficient compilation to the Warren abstract machineButler, Ralph M. / Loganantharaj, Rasiah / Olson, Robert et al. | 1988
- 333
-
Exploitation of parallelism in prototypical deduction problemsButler, Ralph M. / Karonis, Nicholas T. et al. | 1988
- 344
-
A decision procedure for unquantified formulas of graph theoryMoser, Louise E. et al. | 1988
- 358
-
Adventures in associative-commutative unification (A summary)Lincoln, Patrick / Christian, Jim et al. | 1988
- 368
-
Unification in finite algebras is unitary(?)Büttner, Wolfram et al. | 1988
- 378
-
Unification in a combination of arbitrary disjoint equational theoriesSchmidt-Schauß, Manfred et al. | 1988
- 397
-
Partial unification for graph based equational reasoningBläsius, Karl Hans / Siekmann, Jörg H. et al. | 1988
- 415
-
SATCHMO: A theorem prover implemented in PrologManthey, Rainer / Bry, François et al. | 1988
- 435
-
Term rewriting: Some experimental resultsPotter, Richard C. / Plaisted, David A. et al. | 1988
- 454
-
Analogical reasoning and proof discoveryBrock, Bishop / Cooper, Shaun / Pierce, William et al. | 1988
- 469
-
Hyper-chaining and knowledge-based theorem provingHines, Larry et al. | 1988
- 487
-
Linear modal deductionsCerro, Luis Fariñas / Herzig, Andreas et al. | 1988
- 500
-
A resolution calculus for modal logicsOhlbach, Hans Jürgen et al. | 1988
- 517
-
Solving disequations in equational theoriesBürckert, Hans-Jürgen et al. | 1988
- 527
-
On word problems in Horn theoriesKounalis, Emmanuel / Rusinowitch, Michael et al. | 1988
- 538
-
Canonical conditional rewrite systemsDershowitz, Nachum / Okada, Mitsuhiro / Sivakumar, G. et al. | 1988
- 550
-
Program synthesis by completion with dependent subtypesJacquet, Paul et al. | 1988
- 563
-
Reasoning about systems of linear inequalitiesKäufl, Thomas et al. | 1988
- 573
-
A subsumption algorithm based on characteristic matricesSocher, Rolf et al. | 1988
- 582
-
A restriction of factoring in binary resolutionRabinov, Arkady et al. | 1988
- 592
-
Supposition-based logic for automated nonmonotonic reasoningBesnard, Philippe / Siegel, Pierre et al. | 1988
- 602
-
Argument-bounded algorithms as a basis for automated termination proofsWalther, Christoph et al. | 1988
- 622
-
Two automated methods in implementation proofsMarcus, Leo / Redmond, Timothy et al. | 1988
- 643
-
A new approach to universal unfication and its application to AC-unificationFranzen, Mark / Henschen, Lawrence J. et al. | 1988
- 658
-
An implementation of a dissolution-based system employing theory linksMurray, Neil V. / Rosenthal, Erik et al. | 1988
- 675
-
Decision procedure for autoepistemic logicNiemelä, Ilkka et al. | 1988
- 685
-
Logical matrix generation and testingMalkin, Peter K. / Martin, Errol P. et al. | 1988
- 694
-
Optimal time bounds for parallel term matchingVerma, Rakesh M. / Ramakrishnan, I. V. et al. | 1988
- 704
-
Challenge equality problems in lattice theoryMcCune, William et al. | 1988
- 710
-
Single axioms in the implicational propositional calculusPfenning, Frank et al. | 1988
- 714
-
Challenge problems focusing on equality and combinatory logic: Evaluating automated theorem-proving programsWos, Larry / McCune, William et al. | 1988
- 730
-
Challenge problems from nonassociative rings for theorem proversStevens, Rick L. et al. | 1988
- 735
-
An interactive enhancement to the Boyer-Moore theorem proverKaufmann, Matt et al. | 1988
- 737
-
A goal directed theorem proverPlaisted, David A. et al. | 1988
- 738
-
m-NEVER system summaryPase, Bill / Kromodimoeljo, Sentot et al. | 1988
- 740
-
EFS — An interactive Environment for Formal SystemsGriffin, Timothy G. et al. | 1988
- 742
-
Ontic: A knowledge representation system for mathematicsMcAllester, David et al. | 1988
- 744
-
Some tools for an inference laboratory (ATINF)Tour, Thierry Boy / Caferra, Ricardo / Chaminade, Gilles et al. | 1988
- 746
-
Quantlog: A system for approximate reasoning in inconsistent formal systemsSubrahmanian, V. S. / Umrigar, Zerksis D. et al. | 1988
- 748
-
LP: The larch proverGarland, Stephen J. / Guttag, John V. et al. | 1988
- 750
-
The KLAUS automated deduction systemStickel, Mark E. et al. | 1988
- 752
-
A Prolog technology theorem proverStickel, Mark E. et al. | 1988
- 754
-
λProlog: An extended logic programming languageFelty, Amy / Gunter, Elsa / Hannan, John / Miller, Dale / Nadathur, Gopalan / Scedrov, Andre et al. | 1988
- 756
-
SYMEVAL: A theorem prover based on the experimental logicDr. Brown, Frank M. / Park, Seung S. et al. | 1988
- 758
-
ZPLAN: An automatic reasoning system for situationsDr. Brown, Frank M. / Park, Seung S. / Phelps, Jim et al. | 1988
- 760
-
The TPS theorem proving systemAndrews, Peter B. / Issar, Sunil / Nesmith, Daniel / Pfenning, Frank et al. | 1988
- 762
-
MOLOG: A modal PROLOGBieber, Pierre / Fariñas del Cerro, Luis / Herzig, Andreas et al. | 1988
- 764
-
PARTHENON: A parallel theorem prover for non-horn clausesAllen, P. E. / Bose, S. / Clarke, E. M. / Michaylov, S. et al. | 1988
- 766
-
An nH-Prolog implementationSmith, Bruce T. / Loveland, Donald W. et al. | 1988
- 768
-
RRL: A rewrite rule laboratoryKapur, Deepak / Zhang, Hantao et al. | 1988
- 770
-
Geometer: A theorem prover for algebraic geometryCyrluk, David A. / Harris, Richard M. / Kapur, Deepak et al. | 1988
- 772
-
Isabelle: The next seven hundred theorem proversPaulson, Lawrence C et al. | 1988
- 774
-
The CHIP system : Constraint handling in PrologDincbas, M. / Hentenryck, P. / Simonis, H. / Aggoun, A. / Herold, A. et al. | 1988