The following pages link to SPASS (Q16295):
Displaying 50 items.
- Unsorted functional translations (Q2825403) (← links)
- Formalization of the Resolution Calculus for First-Order Logic (Q2829269) (← links)
- Detection of First Order Axiomatic Theories (Q2849492) (← links)
- Presenting and explaining Mizar (Q2867936) (← links)
- An interactive derivation viewer (Q2867942) (← links)
- Automatic Generation of Invariants for Circular Derivations in SUP(LA) (Q2891451) (← links)
- More SPASS with Isabelle (Q2914754) (← links)
- Unifying Theories of Programming in Isabelle (Q2948230) (← links)
- Splitting through New Proposition Symbols (Q2996161) (← links)
- First-Order Atom Definitions Extended (Q2996171) (← links)
- The TPTP World – Infrastructure for Automated Reasoning (Q3066085) (← links)
- Superposition Modulo Non-linear Arithmetic (Q3172887) (← links)
- Translating a Dependently-Typed Logic to First-Order Logic (Q3184740) (← links)
- Simulation and Synthesis of Deduction Calculi (Q3185770) (← links)
- Implementing the Binding and Accommodation Theory for Anaphora Resolution and Presupposition Projection (Q3225401) (← links)
- Proof Verification Technology and Elementary Physics (Q3296311) (← links)
- Mining the Archive of Formal Proofs (Q3453102) (← links)
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP (Q3453107) (← links)
- History and Prospects for First-Order Automated Deduction (Q3454079) (← links)
- Automated Reasoning in the Wild (Q3454081) (← links)
- Ordered Resolution for Coalition Logic (Q3455769) (← links)
- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties (Q3498479) (← links)
- ATP Cross-Verification of the Mizar MPTP Challenge Problems (Q3498492) (← links)
- (Q3509041) (← links)
- Automated Reasoning About Metric and Topology (Q3533154) (← links)
- SMELS: Satisfiability Modulo Equality with Lazy Superposition (Q3540073) (← links)
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) (Q3541699) (← links)
- Subterm contextual rewriting (Q3568223) (← links)
- CTL-RP: A computation tree logic resolution prover (Q3568224) (← links)
- Classification results in quasigroup and loop theory via a combination of automated reasoning tools. (Q3568690) (← links)
- Reasoning Support for Casl with Automated Theorem Proving Systems (Q3591069) (← links)
- System for Automated Deduction (SAD): A Tool for Proof Verification (Q3608785) (← links)
- System Description: Spass Version 3.0 (Q3608799) (← links)
- Automatic Construction and Verification of Isotopy Invariants (Q3613399) (← links)
- (Q4242056) (← links)
- (Q4249898) (← links)
- (Q4263167) (← links)
- (Q4411849) (← links)
- (Q4412857) (← links)
- (Q4413895) (← links)
- An empirical analysis of modal theorem provers (Q4443417) (← links)
- Resolution-based methods for modal logics (Q4487263) (← links)
- (Q4536748) (← links)
- (Q4539595) (← links)
- (Q4539620) (← links)
- Reasoning without believing: on the mechanisation of presuppositions and partiality (Q4583173) (← links)
- SPASS & FLOTTER version 0.42 (Q4647508) (← links)
- (Q4797437) (← links)
- Superposition for Bounded Domains (Q4913861) (← links)
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field (Q4913871) (← links)
