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)
- Fair Derivations in Monodic Temporal Reasoning
- Heaps and Data Structures: A Challenge for Automated Provers
- Blocking and other enhancements for bottom-up model generation methods
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- An efficient subsumption test pipeline for BS(LRA) clauses
- Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL
- Local reductions for the modal cube
- SCL(EQ): SCL for first-order logic with equality
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- AC simplifications and closure redundancies in the superposition calculus
- An interactive derivation viewer
- checkbashisms
- Automated deduction -- CADE-21. 21st international conference on automated deduction, Bremen, Germany, July 17--20, 2007. Proceedings
- The blossom of finite semantic trees
- Institution-based encoding and verification of simple UML state machines in CASL/SPASS
- Subterm contextual rewriting
- Title not available (Why is that?)
- Title not available (Why is that?)
- Combining top-down and bottom-up techniques in program derivation
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- Title not available (Why is that?)
- Verification, Model Checking, and Abstract Interpretation
- GRUNGE: a grand unified ATP challenge
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- Implementing Superposition in iProver (System Description)
- An assumption-based approach for solving the minimal S5-satisfiability problem
- A generic framework for implicate generation modulo theories
- Superposition for \(\lambda\)-free higher-order logic
- Unifying theories of programming in Isabelle
- From search to computation: redundancy criteria and simplification at work
- Superposition modulo non-linear arithmetic
- Unification with abstraction and theory instantiation in saturation-based reasoning
- Automated deduction techniques for the management of personalized documents
- Handling transitive relations in first-order automated reasoning
- CoLiS
- Shellcheck
- Introducing \(H\), an institution-based formal specification and verification language
- CrystalBall
- History and prospects for first-order automated deduction
- Local is best: efficient reductions to modal logic \textsf{K}
- Semantics of Mizar as an Isabelle object logic
- Integration of automated and interactive theorem proving in ILF
- A formally verified interpreter for a shell-like programming language
- On combining algebraic specifications with first-order logic via Athena
- Theorem proving as constraint solving with coherent logic
- A prover dealing with nominals, binders, transitivity and relation hierarchies
- Automating free logic in HOL, with an experimental application in category theory
- Combining proverif and automated theorem provers for security protocol verification
- A resolution calculus for the branching-time temporal logic CTL
- Soft typing for ordered resolution
- Unsorted functional translations
- Combining induction and saturation-based theorem proving
- 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
This page was built for software: SPASS
