OTTER
From MaRDI portal
Software:15442
swMATH2904MaRDI QIDQ15442FDOQ15442
Author name not available (Why is that?)
Official website: https://www.mcs.anl.gov/research/projects/AR/otter/
Cited In (only showing first 100 items - show all)
- User interaction with the Matita proof assistant
- Scavenger 0.1: a theorem prover based on conflict resolution
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- Title not available (Why is that?)
- Title not available (Why is that?)
- INGRID
- Theorema
- TPS
- Title not available (Why is that?)
- Title not available (Why is that?)
- MizarMode
- SATLIB
- MPTP 0.2
- SPASS
- LPL software
- SPASS+T
- STRIP
- Prover9
- FINDER
- DCTP
- I-SATCHMO
- SATCHMO
- SCOTT
- E-Darvin
- MUSCADET
- Mace4
- AURA
- E-SETHEO
- ESC4
- GRAFFITI
- NQTHM
- LOOPS
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- MathXpert
- MBase
- StarExec
- iProver-Eq
- iProver
- MGTP
- leanCoP
- Amphion
- CtCoq
- SAD
- JProver
- leanTAP
- PARTHEO
- Gandalf
- E Theorem Prover
- SicoTHEO
- SbReve2
- Ivy
- MaLARea
- MathWeb
- Analytica
- HR
- Octopus
- tptp2X
- MaGIC
- linTAP
- TABLEAUX
- Roo
- Spartacus
- Metamath
- SMTtoTPTP
- E-MaLeS
- SigmaKEE
- EQP
- HyLoRes
- Tahuti
- Title not available (Why is that?)
- OMEGA
- TRAMP
- BliStrTune
- CLAM
- CLIN
- DISCOUNT
- Lambda-Clam
- LOUI
- Omega-ANTS
- Oyster
- Waldmeister
- XBarnacle
- Prodigy
- Bliksem
- Doris
- P.rex
- PROTEIN
- UCPOP
- Saturate
- Model evolution with equality -- revised and implemented
- MetiTarski: An Automatic Prover for the Elementary Functions
- SAD as a mathematical assistant -- how should we go from here to there?
- The Matita interactive theorem prover
- lean\(T^ AP\): Lean tableau-based deduction
- ProofWatch: watchlist guidance for large theories in E
- Distributed deduction by clause-diffusion: Distributed contraction and the Aquarius prover
- Building Theorem Provers
This page was built for software: OTTER
