chsticksel's library 41 articles Export Sort

Hide details

	Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT [My Copy] Computer Aided Verification 2002 (2002), pp. 681-710. by Clark W. Barrett, David L. Dill, Aaron Stump posted to sat cvc by chsticksel on 2009-12-10 17:39:34 as along with 1 person bfraser
	Efficient Generation of Unsatisfiability Proofs and Cores in SAT [My Copy] In Logic for Programming, Artificial Intelligence, and Reasoning 2008, Vol. 5330 (2008), pp. 16-30. by Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell edited by Iliano Cervesato, Helmut Veith, Andrei Voronkov posted to sat proofs dpll by chsticksel on 2009-12-10 00:16:57 as
	On Finite Satisfiability of Two-Variable First-Order Logic with Equivalence Relations [My Copy] In Logic In Computer Science 2009 (14 August 2009), pp. 123-132. by E. Kieronski, L. Tendera posted to fo_fragment decision_procedure by chsticksel on 2009-12-10 00:03:35 as
	Combinations of Theories for Decidable Fragments of First-Order Logic [My Copy] In Frontiers of Combining Systems 2009 (2009), pp. 263-278. by Pascal Fontaine posted to smt fo_fragment decision_procedure combination by chsticksel on 2009-12-09 23:50:53 as
	Termination Modulo Combinations of Equational Theories [My Copy] In Frontiers of Combining Systems 2009 (2009), pp. 246-262. by Francisco Durán, Salvador Lucas, José Meseguer posted to termination rewriting equational_theory combination by chsticksel on 2009-12-09 23:47:02 as
	Superposition Modulo Linear Arithmetic SUP(LA) [My Copy] In Frontiers of Combining Systems 2009 (2009), pp. 84-99. by Ernst Althaus, Evgeny Kruglov, Christoph Weidenbach posted to superposition linear_arithmetic by chsticksel on 2009-12-09 23:43:48 as
	Combining Equational Reasoning [My Copy] In Frontiers of Combining Systems 2009 (2009), pp. 68-83. by Ashish Tiwari posted to modulo_ac equality combination by chsticksel on 2009-12-09 23:37:39 as
	Elimination of equality via transformation with ordering constraints [My Copy] In Automated Deduction — CADE-15, Vol. 1421 (1998), pp. 175-190. by Leo Bachmair, Harald Ganzinger, Andrei Voronkov edited by Claude Kirchner, Hélène Kirchner posted to ordering equality by chsticksel on 2009-12-09 23:21:14 as
	Real World Verification [My Copy] Automated Deduction – CADE-22 In Automated Deduction – CADE-22 (2009), pp. 485-501. by André Platzer, Jan-David Quesel, Philipp Rümmer posted to real_arithmetic by chsticksel on 2009-12-09 23:08:06 as along with 1 group ACSys
	Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic [My Copy] In Automated Deduction – CADE-22 (2009), pp. 294-305. by Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric Rodríguez-Carbonell, Albert Rubio posted to smt linear_arithmetic by chsticksel on 2009-12-09 23:04:48 as
	Ground Interpolation for Combined Theories [My Copy] In Automated Deduction – CADE-22 (2009), pp. 183-198. by Amit Goel, Sava Krstić, Cesare Tinelli posted to smt interpolation combination by chsticksel on 2009-12-09 23:01:56 as
	veriT: An Open, Trustable and Efficient SMT-Solver [My Copy] In Automated Deduction – CADE-22 (2009), pp. 151-156. by Thomas Bouton, Caminha, David Déharbe, Pascal Fontaine posted to verit system_description smt by chsticksel on 2009-12-09 22:57:57 as
	On Deciding Satisfiability by DPLL(Gamma + T) and Unsound Theorem Proving [My Copy] In Automated Deduction – CADE-22 (2009), pp. 35-50. by Maria Bonacina, Christopher Lynch, Leonardo de Moura posted to superposition smt dpll by chsticksel on 2009-12-09 22:46:50 as
	Superposition and Model Evolution Combined [My Copy] In Automated Deduction – CADE-22 (2009), pp. 17-34. by Peter Baumgartner, Uwe Waldmann posted to superposition model_evolution by chsticksel on 2009-12-09 22:42:09 as
	A Structure-preserving Clause Form Translation [My Copy] Journal of Symbolic Computation, Vol. 2, No. 3. (September 1986), pp. 293-304. by D. Plaisted, S. Greenbaum posted to translation modal_logic by chsticksel on 2009-11-24 18:40:42 as
	Translation Methods for Non-Classical Logics: An Overview [My Copy] Logic Journal of IGPL, Vol. 1, No. 1. (1 July 1993), pp. 69-89. by Hans J. Ohlbach posted to modal_logic by chsticksel on 2009-11-24 18:34:54 as
	Computing finite models by reduction to function-free clause logic [My Copy] Journal of Applied Logic, Vol. 7, No. 1. (March 2009), pp. 58-74. by P. Baumgartner, A. Fuchs, H. Denivelle, C. Tinelli posted to instantiation finite_models epr darwin by chsticksel on 2009-11-24 17:31:50 as
	Paramodulation with Well-founded Orderings [My Copy] Journal of Logic and Computation, Vol. 19, No. 2. (April 2009), pp. 263-302. by Miquel Bofill, Albert Rubio posted to rewriting paramodulation ordering equality by chsticksel on 2009-11-24 17:24:37 as
	Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison [My Copy] Automated Reasoning with Analytic Tableaux and Related Methods, Vol. 1847 (2000), pp. 52-56. by Fabio Massacci, Francesco M. Donini edited by Roy Dyckhoff posted to modal_logic by chsticksel on 2009-11-19 20:01:59 as
	The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0 [My Copy] Journal of Automated Reasoning, Vol. 43, No. 4. (22 July 2009), pp. 337-362. by Geoff Sutcliffe posted to tptp by chsticksel on 2009-11-13 19:00:50 as
	A machine program for theorem-proving [My Copy] Commun. ACM, Vol. 5, No. 7. (July 1962), pp. 394-397. by Martin Davis, George Logemann, Donald Loveland posted to sat dpll by chsticksel on 2009-11-13 18:51:55 as along with 6 people gagliol bsilverthorn bulwahn brothers bfraser voronov
	Resolution Theorem Proving [My Copy] In {Handbook of Automated Reasoning}, Vol. 1 (2001) by Leo Bachmair, Harald Ganzinger edited by Alan Robinson, Andrei Voronkov posted to resolution by chsticksel on 2009-11-13 18:43:26 as
	Logical Engineering with Instance-Based Methods [My Copy] Vol. 4603 (2007), pp. 404-409. by Peter Baumgartner posted to instantiation by chsticksel on 2009-11-13 18:42:27 as
	Instance Based Methods --- An Overview [My Copy] (2009) by Peter Baumgartner, Evgenij Thorstensen posted to oshl model_evolution instantiation inst-gen disconnection by chsticksel on 2009-11-13 18:37:44 as
	Rewrite-Based Decision Procedures [My Copy] Electronic Notes in Theoretical Computer Science In Proceedings of the 6th International Workshop on Strategies in Automated Deduction (STRATEGIES 2006), Vol. 174, No. 11. (July 2007), pp. 27-45. by Maria P. Bonacina, Mnacho Echenim posted to smt rewriting decision_procedure by chsticksel on 2009-11-13 18:36:14 as
	Resolution-Based Methods for Modal Logics [My Copy] Logic Journal of the IGPL, Vol. 8, No. 3. (2000), pp. 265-292. by H. De Nivelle, R. A. Schmidt, U. Hustadt posted to resolution modal_logic decision_procedure by chsticksel on 2009-11-13 18:35:12 as
	Paramodulation-based theorem proving [My Copy] In {Handbook of Automated Reasoning} (1999) by Robert Nieuwenhuis, Albert Rubio edited by Alan Robinson, Andrei Voronkov posted to superposition resolution paramodulation by chsticksel on 2009-11-13 18:31:21 as
	E -- A Brainiac Theorem Prover [My Copy] Journal of AI Communications, Vol. 15, No. 2/3. (2002), pp. 111-126. by Stephan Schulz posted to theorem_prover system_description first_order_logic eprover e by chsticksel on 2009-11-13 18:27:10 as
	CVC: A Cooperating Validity Checker [My Copy] Vol. 2404 (2002), pp. 400-423. by Aaron Stump, Clark W. Barrett, David L. Dill posted to theorem_prover system_description smt cvc3 cvc by chsticksel on 2009-11-13 18:26:20 as
	A DPLL-based Calculus for Ground Satisfiability Modulo Theories [My Copy] Vol. 2424 (2002), pp. 308-319. by Cesare Tinelli edited by Giovambattista Ianni, Sergio Flesca posted to smt dpll by chsticksel on 2009-11-13 18:24:54 as
	Ordered Semantic Hyper-Linking [My Copy] Journal of Automated Reasoning, Vol. 25, No. 3. (1 October 2000), pp. 167-217. by David A. Plaisted, Yunshan Zhu posted to oshl instantiation by chsticksel on 2009-11-06 20:09:35 as
	The Disconnection Tableau Calculus [My Copy] Journal of Automated Reasoning, Vol. 38, No. 1-3. (2 December 2006), pp. 79-126. by Reinhold Letz, Gernot Stenz posted to instantiation disconnection connection by chsticksel on 2009-11-06 20:08:31 as
	New directions in instantiation-based theorem proving [My Copy] Logic in Computer Science, 2003. Proceedings. 18th Annual IEEE Symposium on (09 July 2003), pp. 55-64. by H. Ganzinger, K. Korovin posted to instantiation inst-gen by chsticksel on 2009-11-06 20:07:26 as
	Integrating Equational Reasoning into Instantiation-Based Theorem Proving [My Copy] Computer Science Logic (2004), pp. 71-84. by Harald Ganzinger, Konstantin Korovin posted to instantiation inst-gen equality by chsticksel on 2009-11-06 20:05:21 as
	Theory Instantiation [My Copy] Logic for Programming, Artificial Intelligence, and Reasoning In Lecture Notes in Computer Science, Vol. 4246 (2006), pp. 497-511. by Harald Ganzinger, Konstantin Korovin edited by Miki Hermann, Andrei Voronkov posted to smt instantiation inst-gen by chsticksel on 2009-11-06 20:03:50 as
	An Extensible SAT-solver [My Copy] Theory and Applications of Satisfiability Testing (2004), pp. 333-336. by Niklas Eén, Niklas Sörensson posted to sat minisat dpll decision_procedure by chsticksel on 2009-11-06 20:02:10 as along with 5 people bfraser tuncay mccrimson voronov krauss
	Intelligent Systems and Formal Methods in Software Engineering [My Copy] IEEE Intelligent Systems In Intelligent Systems, Vol. 21, No. 6. (02 November 2006), pp. 71-81. by Bernhard Beckert, Tony Hoare, Reiner Hahnle, et al.Douglas Smith, Cordell Green, Silvio Ranise, Cesare Tinelli, Thomas Ball, Sriram Rajamani posted to no-tag by chsticksel on 2009-11-06 20:00:54 as along with 1 person bfraser
	The Model Evolution Calculus with Equality [My Copy] Automated Deduction – CADE-20 (2005), pp. 392-408. by Peter Baumgartner, Cesare Tinelli posted to model_evolution instantiation equality by chsticksel on 2009-11-06 19:56:40 as
	ME(LIA) - Model Evolution with Linear Integer Arithmetic Constraints [My Copy] Logic for Programming, Artificial Intelligence, and Reasoning In Lecture Notes in Computer Science, Vol. 5330 (2008), pp. 258-273. by Peter Baumgartner, Alexander Fuchs, Cesare Tinelli edited by Iliano Cervesato, Helmut Veith, Andrei Voronkov posted to smt model_evolution instantiation by chsticksel on 2009-11-06 19:29:30 as
	The Model Evolution Calculus [My Copy] Automated Deduction – CADE-19 (2003), pp. 350-364. by Peter Baumgartner, Cesare Tinelli posted to model_evolution instantiation by chsticksel on 2009-10-29 11:27:04 as
	Conflict Resolution [My Copy] Principles and Practice of Constraint Programming - CP 2009 (2009), pp. 509-523. by Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov posted to fourier_motzkin conflict_resolution by chsticksel on 2009-10-29 11:18:14 as along with 1 person and 1 group lilith 8_01

Note: You may cite this page as: http://www.citeulike.org/user/chsticksel

Sort by:
Order:	Default Ascending Descending
Empty fields:	Default First Last

instantiation	11
smt	10
model_evolution	5
equality	5
dpll	5
decision_procedure	5
superposition	4
sat	4
inst-gen	4
modal_logic	4
combination	4
rewriting	3
resolution	3
system_description	3
cvc	2
linear_arithmetic	2
theorem_prover	2
oshl	2
disconnection	2
paramodulation	2
ordering	2
fo_fragment	2
first_order_logic	1
eprover	1
epr	1
termination	1
finite_models	1
modulo_ac	1
connection	1
translation	1
interpolation	1
conflict_resolution	1
equational_theory	1
proofs	1
fourier_motzkin	1
e	1
cvc3	1
darwin	1
minisat	1
tptp	1
real_arithmetic	1
verit	1

chsticksel's library 41 articles Export Sort

chsticksel's tags