msakai's theorem-proving [18 articles] Export

Recent papers added to msakai's library classified by the tag theorem-proving. You can also see everyone's theorem-proving.

Hide details

	補間定理 [My Copy] 一橋論叢, Vol. 100, No. 3. (1988-09-01), pp. 353-366. by 永島, タカシナガシマ, Takashi Nagashima posted to theorem-proving by msakai on 2009-03-17 05:15:10 as along with 1 person hubris
	New Techniques that Improve MACE-style Model Finding [My Copy] In Workshop on Model Computation (MODEL) (2003) by Koen Claessen, Niklas Sörensson posted to model-finding theorem-proving by msakai on 2009-02-22 06:27:22 as along with 1 person bringert
	Using the TPTP Language for Writing Derivations and Finite Interpretations [My Copy] Automated Reasoning (2006), pp. 67-81. by Geoff Sutcliffe, Stephan Schulz, Koen Claessen, Allen Van Gelder posted to theorem-proving by msakai on 2009-02-15 01:41:56 as
	Equinox, A New Theorem Prover for Full First-Order Logic with Equality [My Copy] (October 2005) by Koen Claessen posted to theorem-proving by msakai on 2009-02-02 14:08:28 as
	Rewrite-based Equational Theorem Proving with Selection and Simplification [My Copy] J Logic Computation, Vol. 4, No. 3. (1 June 1994), pp. 217-247. by L. E. O. Bachmair, Harald Ganzinger posted to theorem-proving by msakai on 2009-01-29 15:20:49 as
	Automated Reasoning With Otter [My Copy] (10 January 2001) by John A. Kalman posted to theorem-proving by msakai on 2009-01-07 23:01:16 as
	定理証明系Isabelle/HOLによる計算可能性理論の形式化 [My Copy] by 拓也藤原 posted to theorem-proving by msakai on 2008-12-02 22:02:41 as
	制御系ECU調停器の検証における演繹的アプローチについて (Verifications of an arbiter for electronic control units with an interactive theorem prover) [My Copy] (12 June 2008), pp. 41-47. by Yoshifumi Yuasa, Masakazu Adachi, Noriyoshi Sano posted to agda theorem-proving by msakai on 2008-11-28 03:44:54 as
	Combining Model Checkning and Theorem Proving: A Unified Framework [My Copy] by Sergey Berezin posted to model-checking theorem-proving by msakai on 2008-10-30 06:14:11 as along with 1 person yoriyuki
	From LCF to HOL: a short history [My Copy] (2000), pp. 169-185. by Mike Gordon posted to domain-theory theorem-proving by msakai on 2008-10-07 01:09:43 as
	KAT-ML: An interactive theorem prover for Kleene Algebra with Tests [My Copy] Journal of Applied Non-Classical Logics, Vol. 16 (2003) by Kamal Aboul-Hosn, Dexter Kozen posted to kleene-algebra theorem-proving by msakai on 2008-10-05 16:37:36 as
	The Coq Proof Assistant A Tutorial [My Copy] (8 February 2007) by Gerard Huet, Gilles Kahn, Christine Paulin-Mohring posted to theorem-proving by msakai on 2008-09-03 10:55:39 as along with 2 people GMariano shimomura
	計算と論理のための自然枠組NF/CAL (A Natural Framework for Computation and Logic: NF/CAL) [My Copy] コンピュータソフトウェア, Vol. 23, No. 3. (2006), pp. 3-13. by Masahiko Sato posted to logic theorem-proving by msakai on 2008-06-06 10:59:09 as
	Guarded induction on final coalgebras [My Copy] Electronic Notes in Theoretical Computer Science (January 2004), pp. 1-18. by D. Pavlovic posted to category-theory coalgebra theorem-proving by msakai on 2008-06-01 05:09:27 as along with 1 person christiankissig
	Verifying CPS transformations in Isabelle/HOL [My Copy] In MERLIN '03: Proceedings of the 2003 workshop on Mechanized reasoning about languages with variable binding (2003), pp. 1-8. by Yasuhiko Minamide, Koji Okuma posted to continuation theorem-proving by msakai on 2008-05-28 12:27:00 as along with 2 people and 1 group dalev mvermaat NU-PRL
	Verifying Haskell programs by combining testing, model checking and interactive theorem proving [My Copy] Information and Software Technology In Third International Conference on Quality Software: QSIC 2003, Vol. 46, No. 15. (1 December 2004), pp. 1011-1025. by Peter Dybjer, Qiao Haiyan, Makoto Takeyama posted to haskell model-checking theorem-proving by msakai on 2008-05-28 12:20:45 as along with 2 people pmatos shimomura
	Mechanizing common knowledge logic using COQ [My Copy] Annals of Mathematics and Artificial Intelligence, Vol. 48, No. 1-2. (September 2006), pp. 15-43. by Lescanne, Pierre posted to theorem-proving by msakai on 2007-12-16 04:39:18 as
	An interpolating theorem prover [My Copy] Theoretical Computer Science, Vol. 345, No. 1. (21 November 2005), pp. 101-121. by K. McMillan posted to model-checking theorem-proving by msakai on 2007-11-11 10:38:04 as along with 1 person rhishi

Note: You may cite this page as: http://www.citeulike.org/user/msakai/tag/theorem-proving

category-theory	81
type-theory	80
haskell	59
domain-theory	35
functional	34
model-checking	33
logic	28
ppl2008	26
ppl2009	26
coalgebra	22
continuation	22
theorem-proving	18
program-transformation	17
polymorphism	16
linear-logic	14
linguistics	14
quantum	14
concurrency	12
modal-logic	12
lambda-calculus	11
institution	10
regular-expression	8
algebraic-specification	7
complexity	7
garbage-collection	7
virtual-machine	7
functional-programming	6
logic-programming	6
parametricity	6
aop	5
coq	5
program-analysis	5
rewriting	5
security	5
set-theory	5
agda	4
alloy	4
dependent-types	4
inductive-logic-programming	4
parser	4
reactive	4
ruby	4
specification	4
topology	4
types	4
algebra	3
c	3
compiler	3
game	3
intuitionistic	3
logical-relation	3
machine-learning	3
process-algebra	3
semantics	3
type-classes	3
type-inference	3
unix	3
verification	3
abductive-logic-programming	2
channel-theory	2
chr	2
classical-logic	2
copyright	2
debug	2
denotational-semantics	2
economics	2
encryption	2
filesystem	2
game-semantics	2
kleene-algebra	2
lcm	2
model-finding	2
monad	2
observational-equivalence	2
ontology	2
operational-semantics	2
optimization	2
parallel-programming	2
philosophy	2
physics	2
planning	2
provability	2
slacs2007	2
specialization	2
thermodynamics	2
vaguness	2
algebraic-geometry	1
algorithm	1
answer-set-programming	1
arithmetic	1
arrow	1
baysian-network	1
bdd	1
bignum	1
bug	1
category-thoery	1
chu-space	1
cloud	1
compression	1
constructivity	1
context-free-grammer	1
database	1
deep-inference	1
design-by-contract	1
determinacy	1
dialgebra	1
diff	1
e-mail	1
expression-problem	1
fft	1
finance	1
fix-point	1
functional-logic-programming	1
graph-rewriting	1
gui	1
higher-order-logic	1
history	1
information-theory	1
linear-programming	1
machine-code	1
maude	1
module-system	1
network	1
nuclear-deterrence	1
number-theory	1
ocaml	1
pretty-printing	1
prolog	1
quickcheck	1
refactoring	1
region	1
scala	1
self-reference	1
semantic-web	1
shell-programming	1
smt	1
soft-typing	1
software-engineering	1
stage-calculus	1
static-checking	1
stg	1
strictness-analysis	1
temporal-logic	1
termination	1
testing	1
tex	1
web	1
www2005	1

msakai's theorem-proving [18 articles] Export

msakai's tags