SPASS

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
• Automatic construction and verification of isotopy invariants
• Computing Tiny Clause Normal Forms
• Title not available (Why is that?)
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• Superposition and Model Evolution Combined
• 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
• The higher-order prover \textsc{Leo}-II
• Semantically-guided goal-sensitive reasoning: model representation
• Semi-intelligible Isar proofs from machine-generated proofs
• Model-theoretic methods in combined constraint satisfiability
• New results on rewrite-based satisfiability procedures
• Mathematical Knowledge Management
• System for Automated Deduction (SAD): A Tool for Proof Verification
• Mining the Archive of Formal Proofs
• A combined superposition and model evolution calculus
• Automated inference of finite unsatisfiability
• CTL-RP: A computation tree logic resolution prover
• Classification results in quasigroup and loop theory via a combination of automated reasoning tools.
• Using tableau to decide description logics with full role negation and identity
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Computer supported mathematics with \(\Omega\)MEGA
• Title not available (Why is that?)
• Solving quantified verification conditions using satisfiability modulo theories
• Automated verification of refinement laws
• On the modelling of search in theorem proving -- towards a theory of strategy analysis
• An empirical analysis of modal theorem provers
• LEO-II
• MizarMode
• CASL
• MPTP 0.2
• MAYA
• MoMM
• SPASS+T
• Evaluating general purpose automated theorem proving systems
• Title not available (Why is that?)
• CERES
• Herod
• iProver-Eq
• Pilate
• CalcCheck
• Equinox
• iProver
• TeMP
• HyLoTab
• Sledgehammer: judgement day
• OMEGA
• CLIN
• DISCOUNT
• Lambda-Clam
• LOUI
• Denali
• GAPT
• ProofTool
• Peers-mcd
• Scavenger
• leanK
• Twee
• FLOTTER
• PARIS
• Network Security Policy Verification
• Theorem proving in large formal mathematics as an emerging AI field
• Sqrt_Babylonian
• WhaleProver
• Model evolution with equality -- revised and implemented
• Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans
• Statically safe program generation with SafeGen
• Adimen-SUMO
• CLProver
• Cancellative Abelian monoids and related structures in refutational theorem proving. II
• Title not available (Why is that?)
• Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
• Case splitting in an automatic theorem prover for real-valued special functions
• 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
• One logic to use them all
• Automated verification of relational while-programs
• Labelled splitting
• More SPASS with Isabelle
• The TPTP World -- infrastructure for automated reasoning
• System Description: Spass Version 3.0
• Metis
• An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
• SPASS \& FLOTTER version 0.42
• Splitting through new proposition symbols
• Automated Reasoning
• Scalable fine-grained proofs for formula processing
• Superposition with lambdas
• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
• Vampire with a brain is a good ITP hammer
• Automated Deduction – CADE-20
• An interactive derivation viewer
• Simulation and synthesis of deduction calculi
• Title not available (Why is that?)

This page was built for software: SPASS