swMATH7543MaRDI QIDQ19570FDOQ19570
Author name not available (Why is that?)
Official website: http://www.cs.utexas.edu/users/boyer/ftp/nqthm/
Cited In (only showing first 100 items - show all)
- IsaCoSy
- Theorem proving in cancellative abelian monoids (extended abstract)
- Orderings for term-rewriting systems
- Title not available (Why is that?)
- Title not available (Why is that?)
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Rewriting with equivalence relations in ACL2
- Foundations of a theorem prover for functional and mathematical uses
- Set theory for verification. I: From foundations to functions
- ACL2
- Structured theory development for a mechanized logic
- ML
- LARCH
- PREVAIL
- Superposition theorem proving for abelian groups represented as integer modules
- VLISP
- OMRS
- PVS
- QingTing1
- UCLID
- HOL
- Nuprl
- AURA
- LISP
- SPIKE
- ACL2s
- HipSpec
- Zeno
- MathXpert
- LCF
- GC
- Jerusat
- LEGO
- SAD
- Milawa
- SbReve2
- Sparkle
- Analytica
- GUARDIAN
- Specware
- Jitawa
- UNITY
- ORME
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- A verified runtime for a verified theorem prover
- Cogent
- ICS
- Cyclist
- STeP
- CoqMT
- CLAM
- HOL90
- InKa
- Oyster
- Angelic Verification
- A3PAT
- ROBDD
- Saturate
- Kit
- GCminor
- reFLect
- Modechart
- Silage
- EROS
- VeriFun
- sprfn
- GETFOL
- Emacs
- QuodLibet
- RDL
- Depth First Search
- FELIX
- AFFIRM
- Presburger Automata
- EVES
- SAEPTUM
- Piton
- Coccinelle
- REVE
- RRL
- Knuth Morris Pratt
- DrACuLa
- VerifyThis
- TAME
- Maximum Cardinality Matching
- Tecton
- Cambridge LCF
- AutoCorres
- DefunT
- ShortestPath
- Mollusc
- TXDT
- IMP2_Binary_Heap
- Imandra
- SAD as a mathematical assistant -- how should we go from here to there?
- IMPS: An interactive mathematical proof system
- Partial and nested recursive function definitions in higher-order logic
- An overview of the Tecton proof system
- Proving theorems by reuse
- Deductive and inductive synthesis of equational programs
This page was built for software: NQTHM
