NQTHM
From MaRDI portal
Cited in
(only showing first 100 items - show all)- A verified common lisp implementation of Buchberger's algorithm in ACL2
- Proof assistants: history, ideas and future
- Operating system verification---an overview
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
- The addition of bounded quantification and partial functions to a computational logic and its theorem prover
- The verified incremental design of a distributed spanning tree algorithm: Extended abstract
- Mechanizing structural induction. I: Formal system
- Mechanizing structural induction. II: Strategies
- Context induction: A proof principle for behavioural abstractions and algebraic implementations
- A semi-algorithm for algebraic implementation proofs
- A verification system for concurrent programs based on the Boyer-Moore prover
- Machine checked proofs of the design of a fault-tolerant circuit
- Theories for mechanical proofs of imperative programs
- Nonconstructive computational mathematics
- Superposition theorem proving for abelian groups represented as integer modules
- ACL2
- Lazy techniques for fully expansive theorem proving
- A proof of the nonrestoring division algorithm and its implementation on an ALU
- A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
- Set theory for verification. I: From foundations to functions
- IMPS: An interactive mathematical proof system
- Deductive and inductive synthesis of equational programs
- Introduction to the OBDD algorithm for the ATP community
- Annotations in formal specifications and proofs
- A mechanically verified incremental garbage collector
- On proving the termination of algorithms by machine
- An overview of the Tecton proof system
- Proving Ramsey's theory by the cover set induction: A case and comparision study.
- The application of automated reasoning to questions in mathematics and logic
- Verifying a distributed list system: A case history
- A mechanical proof of Segall's PIF algorithm
- Program tactics and logic tactics
- A temporal logic for real-time partial ordering with named transactions
- ML
- Verification of the Miller-Rabin probabilistic primality test.
- Constraint contextual rewriting.
- PREVAIL
- LARCH
- VLISP
- OMRS
- Structured theory development for a mechanized logic
- PVS
- Convergence: integrating termination and abort-freedom
- QingTing1
- UCLID
- Fermat, Euler, Wilson -- three case studies in number theory
- Incorporating quotation and evaluation into Church's type theory
- HOL
- An assertional proof for a construction of an atomic variable
- Structuring and automating hardware proofs in a higher-order theorem- proving environment
- Algebraic models of microprocessors architecture and organisation
- An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem
- The automated proof of a trace transformation for a bitonic sort
- Automata-driven automated induction
- Cancellative Abelian monoids and related structures in refutational theorem proving. I
- Using eternity variables to specify and prove a serializable database interface
- Nuprl
- Mechanical verification on strategies
- Bounded delay for a free address
- A Ramsey theorem in Boyer-Moore logic
- AURA
- Induction using term orders
- New uses of linear arithmetic in automated theorem proving by induction
- Middle-out reasoning for synthesis and induction
- Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
- LISP
- From Kepler to Hales, and back to Hilbert
- Special issue: Formal proof
- A mechanization of unity in PC-NQTHM-92
- ACL2s
- Zeno
- HipSpec
- Proving theorems by reuse
- Specification and proof in membership equational logic
- MathXpert
- LCF
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- Inductive benchmarks for automated reasoning
- GC
- Jerusat
- LEGO
- SAD
- Sparkle
- Milawa
- SbReve2
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- SPIKE
- GUARDIAN
- Analytica
- Milestones from the Pure Lisp Theorem Prover to ACL2
- Combining induction and saturation-based theorem proving
- Limited second-order functionality in a first-order setting
- A framework for the verification of certifying computations
- Specification and verification of concurrent programs through refinements
- Specware
- Proof movie -- a proof with the Boyer-Moore prover
- A taxonomy of exact methods for partial Max-SAT
- A reconstruction and extension of Maple's assume facility via constraint contextual rewriting
- Jitawa
This page was built for software: NQTHM
