A superposition decision procedure for the guarded fragment with equality
- 20 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
No abstract availableThis publication has 8 references indexed in Scilit:
- Superposition with simplification as a decision procedure for the monadic class with equalityPublished by Springer Nature ,2005
- The two-variable guarded fragment with transitive relationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Basic paramodulation and decidable theoriesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- A non-elementary speed-up in proof length by structural clause form transformationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- SPASS - Version 0.49Journal of Automated Reasoning, 1997
- Ordered paramodulation and resolution as decision procedurePublished by Springer Nature ,1993
- Proving refutational completeness of theorem-proving strategiesJournal of the ACM, 1991
- On restrictions of ordered paramodulation with simplificationPublished by Springer Nature ,1990