Some options:
METIS_TAC[]
works because first-ordering reasoning with equality is certainly
able to find simple substitutions like this one
SRW_TAC[][]
works because SRW_TAC[][] eliminates simple equalities in the
assumptions, whether they are oriented var = expression or
[We apologize if you have received multiple copies of this message]
*
--GandALF 2014-
*
5th International Symposium on Games,
Fourth Summer School on Formal Techniques
May 19 - May 23, 2014
Menlo College, Atherton, CA
http://fm.csl.sri.com/SSFT14
Techniques based on formal logic, such as model checking,
satisfiability, static analysis, and automated theorem proving, are
finding a broad range of applications in modeling,
Hi,
While proving a lemma, I get to this step:
Count winner v = max
0. ((winner' = winner) ∧ (max' = max)) ∧ winner ≠ 0 ⇒
(Count winner v = max)
1. Max_vote n v = (winner',max')
2. Count (SUC n) v > max'
3. SUC n =
SCSS 2014
Symbolic Computation in Software Science
6th International Symposium
Second Call for Papers
Gammarth, La Marsa, Tunisia, December 7-11, 2014
http://www.easychair.org/smart-program/SCSS2014/
Scope
The purpose of SCSS 2014 is to promote research on theoretical and practical
[Apologies if you receive multiple copies of this message]
CALL FOR PAPERS VSTTE 2014
**
6th Working Conference on Verified Software: Theories, Tools, and Experiments
July 17 - 18, 2014
Vienna, Austria
http://vsl2014.at/vstte/
--- Blind-Carbon-Copy
Subject: VeriSure 2014 Call for Papers
X-Mailer: MH-E 8.5; nmh 1.3; GNU Emacs 23.3.1
Date: Thu, 01 May 2014 17:42:30 -0700
Message-ID: <25377.1398991350@ubi>
From: Sam Owre
Bcc: Blind Distribution List: ;
VeriSure 2014: CAV Workshop on Verification and Assurance
CFP: 11th International Workshop on Boolean Problems (IWSBP’14)
Freiberg (Sachs.), Germany, September 17 - 19, 2014
http://www.informatik.tu-freiberg.de/prof2/ws_bp11/index.html
Important Dates:
Submission deadline: April 30, 2014
Notification of acceptance: June 6, 2014
Final version due
On Tue, Apr 29, 2014 at 5:51 AM, Bill Richter wrote:
>
> Here's a more substantive point that's always bothered me. Suppose if one
> is working in one's preferred logical framework (e.g. ZFC), and one engages
> in metamathematics. On what grounds to we believe the metamathematics?
> The poin
