The following pages link to SPASS (Q16295):
Displayed 50 items.
- The higher-order prover \textsc{Leo}-II (Q287283) (← links)
- Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Case splitting in an automatic theorem prover for real-valued special functions (Q352970) (← links)
- Model evolution with equality -- revised and implemented (Q429586) (← links)
- A combined superposition and model evolution calculus (Q438531) (← links)
- Automated inference of finite unsatisfiability (Q438540) (← links)
- Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans (Q475379) (← links)
- Statically safe program generation with SafeGen (Q532402) (← links)
- Model-theoretic methods in combined constraint satisfiability (Q556677) (← links)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915) (← links)
- Vampire with a brain is a good ITP hammer (Q831938) (← links)
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments (Q841684) (← links)
- Representing and building models for decidable subclasses of equational clausal logic (Q861367) (← links)
- Octopus: combining learning and parallel search (Q861370) (← links)
- Applying SAT solving in classification of finite algebras (Q862393) (← links)
- \textit{Theorema}: Towards computer-aided mathematical theory exploration (Q865646) (← links)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- Automatic construction and verification of isotopy invariants (Q928664) (← links)
- Labelled splitting (Q1037396) (← links)
- Automated verification of refinement laws (Q1037397) (← links)
- Solving quantified verification conditions using satisfiability modulo theories (Q1037401) (← links)
- A new methodology for developing deduction methods (Q1037405) (← links)
- On the modelling of search in theorem proving -- towards a theory of strategy analysis (Q1281504) (← links)
- Limited resource strategy in resolution theorem proving (Q1404979) (← links)
- Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators (Q1432885) (← links)
- Deciding the \(E^+\)-class by an a posteriori, liftable order (Q1577484) (← links)
- Evaluating general purpose automated theorem proving systems (Q1606324) (← links)
- SAT-based decision procedures for classical modal logics (Q1610667) (← links)
- Using resolution for testing modal satisfiability and building models (Q1610669) (← links)
- A formally verified interpreter for a shell-like programming language (Q1630019) (← links)
- Formalization of the resolution calculus for first-order logic (Q1663242) (← links)
- A deontic logic reasoning infrastructure (Q1670720) (← links)
- Superposition with structural induction (Q1687553) (← links)
- On combining algebraic specifications with first-order logic via Athena (Q1697091) (← links)
- Semantically-guided goal-sensitive reasoning: inference system and completeness (Q1707598) (← links)
- An assumption-based approach for solving the minimal S5-satisfiability problem (Q1799062) (← links)
- Superposition for \(\lambda\)-free higher-order logic (Q1799065) (← links)
- A generic framework for implicate generation modulo theories (Q1799090) (← links)
- Efficient encodings of first-order Horn formulas in equational logic (Q1799100) (← links)
- A resolution-based calculus for preferential logics (Q1799110) (← links)
- Automated deduction techniques for the management of personalized documents (Q1810920) (← links)
- Cancellative Abelian monoids and related structures in refutational theorem proving. II (Q1864899) (← links)
- Deciding the guarded fragments by resolution (Q1867216) (← links)
- Knowledge-based proof planning (Q1978469) (← links)
- CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications (Q2037935) (← links)
- Improving ENIGMA-style clause selection while learning from history (Q2055886) (← links)
- Handling transitive relations in first-order automated reasoning (Q2069868) (← links)