Cited in
(19)- A note on assumptions about Skolem functions
- Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- Effective normalization techniques for HOL
- Automated verification of refinement laws
- On the modelling of search in theorem proving -- towards a theory of strategy analysis
- SPASS
- Saturate
- METEOR
- KoMeT
- Deciding the guarded fragments by resolution
- Cancellative Abelian monoids and related structures in refutational theorem proving. II
- From search to computation: redundancy criteria and simplification at work
- Integration of automated and interactive theorem proving in ILF
- Labelled splitting
- An optimality result for clause form translation
- Reasoning without believing: on the mechanisation of presuppositions and partiality
- Soft typing for ordered resolution
- Deciding the E^+-class by an a posteriori, liftable order
This page was built for software: FLOTTER
