A theorem prover for a computational logic
From MaRDI portal
Recommendations
Cites work
- A Machine-Oriented Logic Based on the Resolution Principle
- A mechanical proof of the Church-Rosser theorem
- A mechanical proof of the termination of Takeuchi's function
- A Mechanical Proof of the Unsolvability of the Halting Problem
- An axiomatic basis for computer programming
- An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem
- Computer proofs in group theory
- Computer proofs of limit theorems
- Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm
- scientific article; zbMATH DE number 3938596 (Why is no real title available?)
- scientific article; zbMATH DE number 4112064 (Why is no real title available?)
- scientific article; zbMATH DE number 3702108 (Why is no real title available?)
- scientific article; zbMATH DE number 3748393 (Why is no real title available?)
- scientific article; zbMATH DE number 41286 (Why is no real title available?)
- scientific article; zbMATH DE number 88983 (Why is no real title available?)
- scientific article; zbMATH DE number 193479 (Why is no real title available?)
- scientific article; zbMATH DE number 3568056 (Why is no real title available?)
- scientific article; zbMATH DE number 3231608 (Why is no real title available?)
- scientific article; zbMATH DE number 3248792 (Why is no real title available?)
- scientific article; zbMATH DE number 3280051 (Why is no real title available?)
- scientific article; zbMATH DE number 3299649 (Why is no real title available?)
- scientific article; zbMATH DE number 3302923 (Why is no real title available?)
- scientific article; zbMATH DE number 3322506 (Why is no real title available?)
- On the role of automated theorem proving in the compile-time derivation of concurrency
- Proof Checking the RSA Public Key Encryption Algorithm
- Proving Properties of Programs by Structural Induction
- Proving Theorems about LISP Functions
- Reaching Agreement in the Presence of Faults
- Recursive functions of symbolic expressions and their computation by machine, Part I
- Splitting and reduction heuristics in automatic theorem proving
- The addition of bounded quantification and partial functions to a computational logic and its theorem prover
- The automated proof of a trace transformation for a bitonic sort
- The Byzantine Generals Problem
- The Concept of Demodulation in Theorem Proving
- Towards mechanical metamathematics
Cited in
(23)- The addition of bounded quantification and partial functions to a computational logic and its theorem prover
- A circumscriptive theorem prover
- Structured theory development for a mechanized logic
- Fermat, Euler, Wilson -- three case studies in number theory
- An interactive calculus theorem-prover for continuity properties
- Induction using term orders
- Combining induction and saturation-based theorem proving
- Proof movie -- a proof with the Boyer-Moore prover
- Tactic-based inductive theorem prover for data types with partial operations (Diss., Univ. Kaiserslautern, 1999)
- Zeno: an automated prover for properties of recursive data structures
- A theorem prover for Boolean BI
- scientific article; zbMATH DE number 3880145 (Why is no real title available?)
- scientific article; zbMATH DE number 4164171 (Why is no real title available?)
- An Evaluation Based Theorem Prover
- scientific article; zbMATH DE number 4049001 (Why is no real title available?)
- A mechanical proof of the Church-Rosser theorem
- scientific article; zbMATH DE number 88983 (Why is no real title available?)
- scientific article; zbMATH DE number 193479 (Why is no real title available?)
- Foundations of a theorem prover for functional and mathematical uses
- Theorem Proving in Higher Order Logics
- A machine program for theorem-proving
- An extension of the Boyer-Moore theorem prover to support first-order quantification
- Some techniques for reasoning automatically on co-inductive data structures
This page was built for publication: A theorem prover for a computational logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6488518)
