×

zbMATH — the first resource for mathematics

Automated reasoning. 7th international joint conference, IJCAR 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 19–22, 2014. Proceedings. (English) Zbl 1293.68021
Lecture Notes in Computer Science 8562. Lecture Notes in Artificial Intelligence. Berlin: Springer (ISBN 978-3-319-08586-9/pbk). xxviii, 528 p. (2014).

Show indexed articles as search result.

The articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1245.68010].
Indexed articles:
Avni, Guy; Kupferman, Orna; Tamir, Tami, From reachability to temporal specifications in cost-sharing games, 1-15 [Zbl 1423.68272]
Cortier, Véronique, Electronic voting: how logic can help, 16-25 [Zbl 1423.68064]
Goré, Rajeev, And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL, 26-45 [Zbl 1423.68415]
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy, Unified classical logic completeness. A coinductive pearl, 46-60 [Zbl 1409.68250]
Lindblad, Fredrik, A focused sequent calculus for higher-order logic, 61-75 [Zbl 1423.68421]
Lahav, Ori; Zohar, Yoni, SAT-based decision procedure for analytic pure sequent calculi, 76-90 [Zbl 1433.03025]
Heule, Marijn J. H.; Seidl, Martina; Biere, Armin, A unified proof system for QBF preprocessing, 91-106 [Zbl 1409.68257]
Ansótegui, Carlos; Bonet, Maria Luisa; Giráldez-Cru, Jesús; Levy, Jordi, The fractal dimension of SAT formulas, 107-121 [Zbl 1423.68429]
Chocron, Paula; Fontaine, Pascal; Ringeissen, Christophe, A gentle non-disjoint combination of satisfiability procedures, 122-136 [Zbl 1423.68441]
Echenim, Mnacho; Peltier, Nicolas; Tourret, Sophie, A rewriting strategy to generate prime implicates in equational logic, 137-151 [Zbl 1423.68412]
Baumgartner, Peter; Bax, Joshua; Waldmann, Uwe, Finite quantification in hierarchic theorem proving, 152-167 [Zbl 1423.68407]
Berdine, Josh; Bjørner, Nikolaj, Computing all implied equalities via SMT-based partition refinement, 168-183 [Zbl 1423.68408]
Giesl, Jürgen; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René, Proving termination of programs automatically with AProVE, 184-191 [Zbl 1409.68256]
Horbach, Matthias; Sofronie-Stokkermans, Viorica, Locality transfer: from constrained axiomatizations to reachability predicates, 192-207 [Zbl 1423.68420]
Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter, Proving termination and memory safety for programs with pointer arithmetic, 208-223 [Zbl 1423.68110]
Zhang, Wenhui, QBF encoding of temporal properties and QBF-based verification, 224-239 [Zbl 1423.68296]
Hetzl, Stefan; Leitsch, Alexander; Reis, Giselle; Tapolczai, Janos; Weller, Daniel, Introducing quantified cuts in logic with equality, 240-254 [Zbl 1423.68418]
Nigam, Vivek; Reis, Giselle; Lima, Leonardo, Quati: an automated tool for proving permutation lemmas, 255-261 [Zbl 1423.68422]
Goré, Rajeev; Thomson, Jimmy; Wu, Jesse, A history-based theorem prover for intuitionistic propositional logic using global caching: IntHistGC system description, 262-268 [Zbl 1423.68417]
Otten, Jens, MleanCoP: a connection prover for first-order modal logic, 269-276 [Zbl 1423.68423]
Cerrito, Serenella; David, Amélie; Goranko, Valentin, Optimal tableaux-based decision procedure for testing satisfiability in the alternating-time temporal logic \(\mathrm{ATL}^+\), 277-291 [Zbl 1423.68410]
Jeannin, Jean-Baptiste; Platzer, André, dTL\(^{2}\): differential temporal dynamic logic with nested temporalities for hybrid systems, 292-306 [Zbl 1423.68283]
Lellmann, Björn, Axioms vs hypersequent rules with context restrictions: theory and applications, 307-321 [Zbl 1425.03026]
Nalon, Cláudia; Marcos, João; Dixon, Clare, Clausal resolution for modal logics of confluence, 322-336 [Zbl 1425.03008]
Goré, Rajeev; Olesen, Kerry; Thomson, Jimmy, Implementing tableau calculi using BDDs: BDDTab system description, 337-343 [Zbl 1423.68416]
Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp, Approximations for model construction, 344-359 [Zbl 1409.68264]
Ehlers, Rüdiger; Lange, Martin, A tool that incrementally approximates finite satisfiability in full interval temporal logic, 360-366 [Zbl 1423.68414]
Papacchini, Fabio; Schmidt, Renate A., Terminating minimal model generation procedures for propositional modal logics, 381-395 [Zbl 1423.68289]
Beyersdorff, Olaf; Chew, Leroy, The complexity of theorem proving in circumscription and minimal entailment, 403-417 [Zbl 1425.03006]
Bozzelli, Laura; Sánchez, César, Visibly linear temporal logic, 418-433 [Zbl 1423.68274]
Koopmann, Patrick; Schmidt, Renate A., Count and forget: uniform interpolation of \(\mathcal{SHQ}\)-ontologies, 434-448 [Zbl 1423.68482]
Steigmiller, Andreas; Glimm, Birte; Liebig, Thorsten, Coupling tableau algorithms for expressive description logics with completion-based saturation procedures, 449-463 [Zbl 1423.68486]
Carral, David; Feier, Cristina; Cuenca Grau, Bernardo; Hitzler, Pascal; Horrocks, Ian, \(\mathcal{EL}\)-ifying ontologies, 464-479 [Zbl 1423.68487]
Ceylan, İsmail İlkan; Peñaloza, Rafael, The Bayesian description logic \({\mathcal{BEL}}\), 480-494 [Zbl 1409.68277]
Beeson, Michael; Wos, Larry, OTTER proofs in Tarskian geometry, 495-510 [Zbl 1414.68099]
Olivetti, Nicola; Pozzato, Gian Luca, NESCOND: an implementation of nested sequent calculi for conditional logics, 511-518 [Zbl 1425.68378]

MSC:
68-06 Proceedings, conferences, collections, etc. pertaining to computer science
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
00B25 Proceedings of conferences of miscellaneous specific interest
PDF BibTeX XML Cite
Full Text: DOI