SPASS
From MaRDI portal
swMATH4108MaRDI QIDQ16295FDOQ16295
Author name not available (Why is that?)
Official website: http://www.spass-prover.org/
Cited In (only showing first 100 items - show all)
- Herbrand constructivization for automated intuitionistic theorem proving
- CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- Computing Tiny Clause Normal Forms
- Title not available (Why is that?)
- Superposition and Model Evolution Combined
- The higher-order prover \textsc{Leo}-II
- Semantically-guided goal-sensitive reasoning: model representation
- Semi-intelligible Isar proofs from machine-generated proofs
- New results on rewrite-based satisfiability procedures
- Mathematical Knowledge Management
- Mining the Archive of Formal Proofs
- CTL-RP: A computation tree logic resolution prover
- Computer supported mathematics with \(\Omega\)MEGA
- Automated verification of refinement laws
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- Evaluating general purpose automated theorem proving systems
- Sledgehammer: judgement day
- OMEGA
- TRAMP
- Leo-III
- miz3
- IsaFoL
- CafeInMaude
- CLIN
- DISCOUNT
- Leo
- Lambda-Clam
- LOUI
- Waldmeister
- Prodigy
- Bliksem
- Doris
- E-KRHyper
- 3TAP
- IDV
- KOMET
- Medmaker
- Multi
- P.rex
- PROTEIN
- Denali
- Saturate
- GAPT
- SRASS
- ProofTool
- SPTHEO
- LoAT
- InKreSAT
- mural
- Peers-mcd
- Scavenger
- TAMARIN
- CTL-RP
- PARTHENON
- METEOR
- Aquarius
- AVATAR
- HGen
- FOL Fitting
- Abstract Soundness
- Incompleteness Theorems
- Logic2CNF
- leanK
- Psyche
- KoMeT
- KL-ONE
- Twee
- FLOTTER
- PARIS
- Omega-MKRP
- AxiomaticCategoryTheory
- GoedelGod
- CoDe
- Network Security Policy Verification
- GKC
- Regular_Algebras
- Theorem proving in large formal mathematics as an emerging AI field
- Sqrt_Babylonian
- Zipperposition
- Slakje
- WhaleProver
- CiMPG
- Adimen-SUMO
- GNU parallel
- Ordered_Resolution_Prover
- CLProver
- CrEme
- SPASS-AR
- SAD as a mathematical assistant -- how should we go from here to there?
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- On interpolation in automated theorem proving
- Premise selection for mathematics by corpus analysis and kernel methods
- The model evolution calculus as a first-order DPLL method
- More SPASS with Isabelle
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
- SPASS \& FLOTTER version 0.42
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- System for Automated Deduction (SAD): A Tool for Proof Verification
This page was built for software: SPASS
