Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments. (English) Zbl 07800192
MSC:
68V15
Found 17 Documents (Results 1–17)
SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment. (English) Zbl 1468.68308
Modal satisfiability via SMT solving. (English) Zbl 1453.03015
De Nicola, Rocco (ed.) et al., Software, services, and systems. Essays dedicated to Martin Wirsing on the occasion of his retirement from the chair of programming and software engineering, Munich, Germany, 2015. Essays. Cham: Springer. Lect. Notes Comput. Sci. 8950, 30-45 (2015).
First-order resolution methods for modal logics. (English) Zbl 1383.03031
Voronkov, Andrei (ed.) et al., Programming logics. Essays in memory of Harald Ganzinger. Berlin: Springer (ISBN 978-3-642-37650-4/pbk). Lecture Notes in Computer Science 7797, 345-391 (2013).
From search to computation: redundancy criteria and simplification at work. (English) Zbl 1383.68076
Voronkov, Andrei (ed.) et al., Programming logics. Essays in memory of Harald Ganzinger. Berlin: Springer (ISBN 978-3-642-37650-4/pbk). Lecture Notes in Computer Science 7797, 169-193 (2013).
Harald Ganzinger’s legacy: contributions to logics and programming. (English) Zbl 1383.68003
Voronkov, Andrei (ed.) et al., Programming logics. Essays in memory of Harald Ganzinger. Berlin: Springer (ISBN 978-3-642-37650-4/pbk). Lecture Notes in Computer Science 7797, 1-18 (2013).
Superposition decides the first-order logic fragment over ground theories. (English) Zbl 1262.68160
MSC:
68T15
03B25
Superposition as a decision procedure for timed automata. (English) Zbl 1262.68159
MSC:
68T15
03B25
Superposition for fixed domains. (English) Zbl 1156.03313
Kaminski, Michael (ed.) et al., Computer science logic. 22nd international workshop, CSL 2008, 17th annual conference of the EACSL, Bertinoro, Italy, September 16–19, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-87530-7/pbk). Lecture Notes in Computer Science 5213, 293-307 (2008).
Automated theorem proving by resolution in non-classical logics. (English) Zbl 1130.03010
Reviewer: Nail Zamov (Kazan)
MSC:
03B35
Modular proof systems for partial functions with Evans equality. (English) Zbl 1103.68112
MSC:
68T15
03B35
MPTP 0.1 – system description. (English) Zbl 1261.68107
Dahn, Ingo (ed.) et al., FTP’2003: 4th international workshop on first-order theorem proving. Proceedings of the workshop (in connection with RDP’03, federated conference on rewriting, deduction and programming), Valencia, Spain, June 12–14, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 86, No. 1, 147-152 (2003).
MSC:
68T15
Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators. (English) Zbl 1043.03013
Filter Results by …
Document Type
- Journal Articles (11)
- Collection Articles (6)
all
top 5
Author
- Weidenbach, Christoph (6)
- Schmidt, Renate A. (3)
- Sofronie-Stokkermans, Viorica (3)
- Hustadt, Ullrich (2)
- Waldmann, Uwe (2)
- Areces, Carlos (1)
- Baumgartner, Peter (1)
- Fietzke, Arnaud (1)
- Fontaine, Pascal (1)
- Ganzinger, Harald (1)
- Georgieva, Lilia (1)
- Hillenbrand, Thomas (1)
- Horbach, Matthias (1)
- Jacquemard, Florent (1)
- Kapur, Deepak (1)
- Kruglov, Evgeniĭ Valentinovich (1)
- Merz, Stephan (1)
- Nieuwenhuis, Robert (1)
- Ohta, Yoshikatsu (1)
- Oyamaguchi, Michio (1)
- Piskac, Ruzica (1)
- Rusinowitch, Michaël (1)
- Teucke, Andreas (1)
- Tinelli, Cesare (1)
- Urban, Josef (1)
- Vigneron, Laurent (1)
- Voronkov, Andrei (1)
- Wilhelm, Reinhard (1)
- Zheng, Sen (1)
all
top 5
Serial
- J. Symb. Comput. (2)
- Inf. Comput. (2)
- J. Autom. Reasoning (2)
- Math. Comput. Sci. (2)
- Artif. Intell. (1)
- Ann. Math. Artif. Intell. (1)
- J. Log. Algebr. Program. (1)
