SPASS

swMATH4108MaRDI QIDQ16295

No author found.

Related Items (only showing first 100 items - show all)

Heterogeneous heuristic optimisation and scheduling for first-order theorem proving ⋮ The higher-order prover \textsc{Leo}-II ⋮ Semantically-guided goal-sensitive reasoning: model representation ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Vampire with a brain is a good ITP hammer ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A formally verified interpreter for a shell-like programming language ⋮ Assumption propagation through annotated programs ⋮ ATP-based cross-verification of Mizar proofs: method, systems, and first experiments ⋮ From informal to formal proofs in Euclidean geometry ⋮ AC simplifications and closure redundancies in the superposition calculus ⋮ The model evolution calculus as a first-order DPLL method ⋮ Proof planning with multiple strategies ⋮ Representing and building models for decidable subclasses of equational clausal logic ⋮ Octopus: combining learning and parallel search ⋮ Applying SAT solving in classification of finite algebras ⋮ \textit{Theorema}: Towards computer-aided mathematical theory exploration ⋮ Computer supported mathematics with \(\Omega\)MEGA ⋮ SAD as a mathematical assistant -- how should we go from here to there? ⋮ Case splitting in an automatic theorem prover for real-valued special functions ⋮ Crystal: Integrating structured queries into a tactic language ⋮ Formalization of the resolution calculus for first-order logic ⋮ A deontic logic reasoning infrastructure ⋮ Commonsense reasoning about containers using radically incomplete information ⋮ Herbrand constructivization for automated intuitionistic theorem proving ⋮ Introducing \(H\), an institution-based formal specification and verification language ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Superposition with structural induction ⋮ Pattern-based and composition-driven automatic generation of logical specifications for workflow-oriented software models ⋮ On combining algebraic specifications with first-order logic via Athena ⋮ Limited resource strategy in resolution theorem proving ⋮ Resolution with order and selection for hybrid logics ⋮ Model evolution with equality -- revised and implemented ⋮ Theorem proving using clausal resolution: from past to present ⋮ A combined superposition and model evolution calculus ⋮ Automated inference of finite unsatisfiability ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ Automatic construction and verification of isotopy invariants ⋮ Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators ⋮ Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans ⋮ Automated deduction -- CADE-21. 21st international conference on automated deduction, Bremen, Germany, July 17--20, 2007. Proceedings ⋮ Knowledge-based proof planning ⋮ Institution-based encoding and verification of simple UML state machines in CASL/SPASS ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ Statically safe program generation with SafeGen ⋮ Resolution in Modal, Description and Hybrid Logic ⋮ Model-theoretic methods in combined constraint satisfiability ⋮ CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications ⋮ An assumption-based approach for solving the minimal S5-satisfiability problem ⋮ Superposition for \(\lambda\)-free higher-order logic ⋮ A generic framework for implicate generation modulo theories ⋮ Efficient encodings of first-order Horn formulas in equational logic ⋮ A resolution-based calculus for preferential logics ⋮ Automated deduction techniques for the management of personalized documents ⋮ Automating free logic in HOL, with an experimental application in category theory ⋮ A prover dealing with nominals, binders, transitivity and relation hierarchies ⋮ Blocking and other enhancements for bottom-up model generation methods ⋮ Combining induction and saturation-based theorem proving ⋮ SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment ⋮ Schematic Cut Elimination and the Ordered Pigeonhole Principle ⋮ Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving ⋮ Effective Normalization Techniques for HOL ⋮ Improving ENIGMA-style clause selection while learning from history ⋮ SPASS-SATT. A CDCL(LA) solver ⋮ GRUNGE: a grand unified ATP challenge ⋮ Combining proverif and automated theorem provers for security protocol verification ⋮ Handling transitive relations in first-order automated reasoning ⋮ On the modelling of search in theorem proving -- towards a theory of strategy analysis ⋮ Labelled splitting ⋮ Automated verification of refinement laws ⋮ Solving quantified verification conditions using satisfiability modulo theories ⋮ A new methodology for developing deduction methods ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Unification with abstraction and theory instantiation in saturation-based reasoning ⋮ Deciding the \(E^+\)-class by an a posteriori, liftable order ⋮ Subsumption demodulation in first-order theorem proving ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ Local is best: efficient reductions to modal logic \textsf{K} ⋮ Theorem proving as constraint solving with coherent logic ⋮ An efficient subsumption test pipeline for BS(LRA) clauses ⋮ Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Local reductions for the modal cube ⋮ A subset-matching size-bounded cache for testing satisfiability in modal logics ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. II ⋮ SMELS: satisfiability modulo equality with lazy superposition ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) ⋮ Evaluating general purpose automated theorem proving systems ⋮ Premise selection for mathematics by corpus analysis and kernel methods ⋮ On interpolation in automated theorem proving ⋮ Deciding the guarded fragments by resolution ⋮ Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry ⋮ SAT-based decision procedures for classical modal logics ⋮ Using resolution for testing modal satisfiability and building models

This page was built for software: SPASS