DAO2011: Ejercicios de deducción natural proposicional con Isabelle/HOL

En la clase de hoy del curso de Demostración asistida por ordenador se han comentado las soluciones de los ejercicios de deducción natural proposicional con Isabelle/HOL/Isar.

A continuación se muestra la teoría correspondiente a los enunciados de los ejercicios

header {* Deducción natural proposicional *}

theory Tema_3_ej
imports Main 
begin 
 
section {* Deducción natural proposicional *}
 
text {* Los ejercicios de esta relación deben de resolverse usando sólo
  las reglas básicas de la deducción natural proposicional: 
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  
  · notnotD:    ¬¬ P ⟹ P
  . notnotI:    P ⟹ ¬¬ P
  · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q 
  · mt:         ⟦F ⟶ G; ¬G⟧ ⟹ ¬F 
  · impI:       (P ⟹ Q) ⟹ P ⟶ Q
  · disjI1:     P ⟹ P ∨ Q
  · disjI2:     Q ⟹ P ∨ Q
  · disjE:      ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R 
  · FalseE:     False ⟹ P
  · notE:       ⟦¬P; P⟧ ⟹ R
  · notI:       (P ⟹ False) ⟹ ¬P
  · iffI:       ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
  · iffD1:      ⟦Q = P; Q⟧ ⟹ P 
  · iffD2:      ⟦P = Q; Q⟧ ⟹ P
  · ccontr:     (¬P ⟹ False) ⟹ P
*}
 
lemma notnotI: "P ⟹ ¬¬ P"
by auto
 
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto
 
lemma ejercicio_1:
  assumes 1: "p ⟶ q" and
          2: "p"
  shows "q"  
oops
 
lemma ejercicio_1b:
  assumes 1: "p ⟶ q" and
          2: "p"
  shows "q"  
oops
 
lemma ejercicio_2:
  assumes 1: "p⟶q" and 
          2: "q⟶r" and 
          3: "p" 
  shows "r"
oops
 
lemma ejercicio_3:
  assumes 1: "p⟶(q⟶r)" and 
          2: "p⟶q" and  
          3: "p"
  shows "r"
oops
 
lemma ejercicio_4:
  assumes 1: "p⟶q" and 
          2: "q⟶r" 
  shows "p⟶r"
oops
 
lemma ejercicio_5:
  assumes 1: "p⟶(q⟶r)"
  shows "q⟶(p⟶r)"
oops
 
lemma ejercicio_6:
  assumes 1: "p⟶(q⟶r)" 
  shows "(p⟶q)⟶(p⟶r)"
oops
 
lemma ejercicio_7:
  assumes 1: "p" 
  shows "q⟶p"
oops
 
lemma ejercicio_8:
  "p⟶(q⟶p)"
oops
 
lemma ejercicio_9:
  assumes 1: "p⟶q"  
  shows "(q⟶r)⟶(p⟶r)"
oops
 
lemma ejercicio_10:
  assumes 1: "p⟶(q⟶(r⟶s))"
  shows "r⟶(q⟶(p⟶s))"
oops
 
lemma ejercicio_11:
  "(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"
oops
 
lemma ejercicio_12:
  assumes 1: "(p⟶q)⟶r" 
  shows "p⟶(q⟶r)"
oops
 
lemma ejercicio_13:
  assumes 1: "p" and  
          2: "q" 
  shows "p∧q"
oops
 
lemma ejercicio_14:
  assumes 1: "p∧q" 
  shows "p"
oops
 
lemma ejercicio_15:
  assumes 1: "p∧q" 
  shows "q"
oops
 
lemma ejercicio_16:
  assumes 1: "p∧(q∧r)"
  shows "(p∧q)∧r"
oops
 
lemma ejercicio_17:
  assumes 1: "(p∧q)∧r"
  shows "p∧(q∧r)"
oops
 
lemma ejercicio_18:
  assumes 1: "p∧q"
  shows "p⟶q"
oops
 
lemma ejercicio_19:
  assumes 1: "(p⟶q)∧(p⟶r)" 
  shows "p⟶q∧r"
oops
 
lemma ejercicio_20:
  assumes 1: "p⟶q∧r" 
  shows "(p⟶q)∧(p⟶r)"
oops
 
lemma ejercicio_21:
  assumes 1: "p⟶(q⟶r)" 
  shows "p∧q⟶r"
oops
 
lemma ejercicio_22:
  assumes 1: "p∧q⟶r"  
  shows "p⟶(q⟶r)"
oops
 
lemma ejercicio_23:
  assumes 1: "(p⟶q)⟶r" 
  shows "p∧q⟶r"
oops
 
lemma ejercicio_24:
  assumes 1: "p∧(q⟶r)"  
  shows "(p⟶q)⟶r"
oops
 
lemma ejercicio_25:
  assumes 1: "p" 
  shows "p∨q"
oops
 
lemma ejercicio_26:
  assumes 1: "q"  
  shows "p∨q"
oops
 
lemma ejercicio_27:
  assumes 1: "p∨q" 
  shows "q∨p"
oops
 
lemma ejercicio_28:
  assumes 1: "q⟶r" 
  shows "p∨q⟶p∨r"
oops
 
lemma ejercicio_29:
  assumes 1: "p∨p" 
  shows "p"
oops
 
lemma ejercicio_30:
  assumes 1: "p" 
  shows "p∨p"
oops
 
lemma ejercicio_31:
  assumes 1: "p∨(q∨r)"
  shows "(p∨q)∨r"
oops
 
lemma ejercicio_32:
  assumes 1: "(p∨q)∨r"
  shows "p∨(q∨r)"
oops
 
lemma ejercicio_33:
  assumes 1: "p∧(q∨r)" 
  shows "(p∧q)∨(p∧r)"
oops
 
lemma ejercicio_34:
  assumes 1: "(p∧q)∨(p∧r)" 
  shows "p∧(q∨r)"
oops
 
lemma ejercicio_35:
  assumes 1: "p∨(q∧r)"
  shows "(p∨q)∧(p∨r)"
oops
 
lemma ejercicio_36:
  assumes 1: "(p∨q)∧(p∨r)"
  shows "p∨(q∧r)"
oops
 
lemma ejercicio_37:
  assumes 1: "(p⟶r)∧(q⟶r)" 
  shows "p∨q⟶r"
oops
 
lemma ejercicio_38:
  assumes 1: "p∨q⟶r"  
  shows "(p⟶r)∧(q⟶r)"
oops
 
lemma ejercicio_39:
  assumes 1: "p"
  shows "¬¬p"
oops
 
lemma ejercicio_40:
  assumes 1: "¬p"  
  shows "p⟶q"
oops
 
lemma ejercicio_41:
  assumes 1: "p⟶q"
  shows "¬q⟶¬p"
oops
 
lemma ejercicio_42:
  assumes 1: "p∨q" and
          2: "¬q" 
  shows "p"
oops
 
lemma ejercicio_43:
  assumes 1: "p∨q" and
          2: "¬p" 
  shows "q"
oops
 
lemma ejercicio_44:
  assumes 1: "p∨q"
  shows "¬(¬p∧¬q)"
oops
 
lemma ejercicio_45:
  assumes 1: "p∧q"
  shows "¬(¬p∨¬q)"
oops
 
lemma ejercicio_46:
  assumes 1: "¬(p∨q)"
  shows "¬p∧¬q"
oops
 
lemma ejercicio_47:
  assumes 1: "¬p∧¬q"  
  shows "¬(p∨q)"
oops
 
lemma ejercicio_48:
  assumes 1: "¬p∨¬q"
  shows "¬(p∧q)"
oops
 
lemma ejercicio_49:
  "¬(p∧¬p)"
oops
 
lemma ejercicio_50:
  assumes 1: "p∧¬p"
  shows "q"
oops
 
lemma ejercicio_51:
  assumes 1: "¬¬p"
  shows "p"
oops
 
lemma ejercicio_52:
  "p∨¬p"
oops
 
lemma ejercicio_53:
  "((p⟶q)⟶p)⟶p"
oops
 
lemma ejercicio_54:
  assumes 1: "¬q⟶¬p"
  shows "p⟶q"
oops
 
lemma ejercicio_55:
  assumes 1: "¬(¬p∧¬q)"
  shows "p∨q"
oops
 
lemma ejercicio_56:
  assumes 1: "¬(¬p∨¬q)"
  shows "p∧q"
oops
 
lemma ejercicio_57:
  assumes 1: "¬(p∧q)"
  shows "¬p∨¬q"
oops
 
lemma ejercicio_58:
  "(p⟶q)∨(q⟶p)"
oops
 
end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

190

191

192

193

194

195

196

197

198

199

200

201

202

203

204

205

206

207

208

209

210

211

212

213

214

215

216

217

218

219

220

221

222

223

224

225

226

227

228

229

230

231

232

233

234

235

236

237

238

239

240

241

242

243

244

245

246

247

248

249

250

251

252

253

254

255

256

257

258

259

260

261

262

263

264

265

266

267

268

269

270

271

272

273

274

275

276

277

278

279

280

281

282

283

284

285

286

287

288

289

290

291

292

293

294

295

296

297

298

299

300

301

302

303

304

305

306

307

308

309

310

311

312

313

314

315

316

317

318

319

320

321

322

323

324

325

326

327

328

329

330

331

332

333

334

335

336

header {* Deducción natural proposicional *}

theory Tema_3_ej

imports Main

begin

section {* Deducción natural proposicional *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo

las reglas básicas de la deducción natural proposicional:

· conjI: ⟦P; Q⟧ ⟹ P ∧ Q

· conjunct1: P ∧ Q ⟹ P

· conjunct2: P ∧ Q ⟹ Q

· notnotD: ¬¬ P ⟹ P

. notnotI: P ⟹ ¬¬ P

· mp: ⟦P ⟶ Q; P⟧ ⟹ Q

· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F

· impI: (P ⟹ Q) ⟹ P ⟶ Q

· disjI1: P ⟹ P ∨ Q

· disjI2: Q ⟹ P ∨ Q

· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R

· FalseE: False ⟹ P

· notE: ⟦¬P; P⟧ ⟹ R

· notI: (P ⟹ False) ⟹ ¬P

· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q

· iffD1: ⟦Q = P; Q⟧ ⟹ P

· iffD2: ⟦P = Q; Q⟧ ⟹ P

· ccontr: (¬P ⟹ False) ⟹ P

lemma notnotI: "P ⟹ ¬¬ P"

by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"

by auto

lemma ejercicio_1:

assumes 1: "p ⟶ q" and

2: "p"

shows "q"

oops

lemma ejercicio_1b:

assumes 1: "p ⟶ q" and

2: "p"

shows "q"

oops

lemma ejercicio_2:

assumes 1: "p⟶q" and

2: "q⟶r" and

3: "p"

shows "r"

oops

lemma ejercicio_3:

assumes 1: "p⟶(q⟶r)" and

2: "p⟶q" and

3: "p"

shows "r"

oops

lemma ejercicio_4:

assumes 1: "p⟶q" and

2: "q⟶r"

shows "p⟶r"

oops

lemma ejercicio_5:

assumes 1: "p⟶(q⟶r)"

shows "q⟶(p⟶r)"

oops

lemma ejercicio_6:

assumes 1: "p⟶(q⟶r)"

shows "(p⟶q)⟶(p⟶r)"

oops

lemma ejercicio_7:

assumes 1: "p"

shows "q⟶p"

oops

lemma ejercicio_8:

"p⟶(q⟶p)"

oops

lemma ejercicio_9:

assumes 1: "p⟶q"

shows "(q⟶r)⟶(p⟶r)"

oops

lemma ejercicio_10:

assumes 1: "p⟶(q⟶(r⟶s))"

shows "r⟶(q⟶(p⟶s))"

oops

lemma ejercicio_11:

"(p⟶(q⟶r))⟶((p⟶q)⟶(p⟶r))"

oops

lemma ejercicio_12:

assumes 1: "(p⟶q)⟶r"

shows "p⟶(q⟶r)"

oops

lemma ejercicio_13:

assumes 1: "p" and

2: "q"

shows "p∧q"

oops

lemma ejercicio_14:

assumes 1: "p∧q"

shows "p"

oops

lemma ejercicio_15:

assumes 1: "p∧q"

shows "q"

oops

lemma ejercicio_16:

assumes 1: "p∧(q∧r)"

shows "(p∧q)∧r"

oops

lemma ejercicio_17:

assumes 1: "(p∧q)∧r"

shows "p∧(q∧r)"

oops

lemma ejercicio_18:

assumes 1: "p∧q"

shows "p⟶q"

oops

lemma ejercicio_19:

assumes 1: "(p⟶q)∧(p⟶r)"

shows "p⟶q∧r"

oops

lemma ejercicio_20:

assumes 1: "p⟶q∧r"

shows "(p⟶q)∧(p⟶r)"

oops

lemma ejercicio_21:

assumes 1: "p⟶(q⟶r)"

shows "p∧q⟶r"

oops

lemma ejercicio_22:

assumes 1: "p∧q⟶r"

shows "p⟶(q⟶r)"

oops

lemma ejercicio_23:

assumes 1: "(p⟶q)⟶r"

shows "p∧q⟶r"

oops

lemma ejercicio_24:

assumes 1: "p∧(q⟶r)"

shows "(p⟶q)⟶r"

oops

lemma ejercicio_25:

assumes 1: "p"

shows "p∨q"

oops

lemma ejercicio_26:

assumes 1: "q"

shows "p∨q"

oops

lemma ejercicio_27:

assumes 1: "p∨q"

shows "q∨p"

oops

lemma ejercicio_28:

assumes 1: "q⟶r"

shows "p∨q⟶p∨r"

oops

lemma ejercicio_29:

assumes 1: "p∨p"

shows "p"

oops

lemma ejercicio_30:

assumes 1: "p"

shows "p∨p"

oops

lemma ejercicio_31:

assumes 1: "p∨(q∨r)"

shows "(p∨q)∨r"

oops

lemma ejercicio_32:

assumes 1: "(p∨q)∨r"

shows "p∨(q∨r)"

oops

lemma ejercicio_33:

assumes 1: "p∧(q∨r)"

shows "(p∧q)∨(p∧r)"

oops

lemma ejercicio_34:

assumes 1: "(p∧q)∨(p∧r)"

shows "p∧(q∨r)"

oops

lemma ejercicio_35:

assumes 1: "p∨(q∧r)"

shows "(p∨q)∧(p∨r)"

oops

lemma ejercicio_36:

assumes 1: "(p∨q)∧(p∨r)"

shows "p∨(q∧r)"

oops

lemma ejercicio_37:

assumes 1: "(p⟶r)∧(q⟶r)"

shows "p∨q⟶r"

oops

lemma ejercicio_38:

assumes 1: "p∨q⟶r"

shows "(p⟶r)∧(q⟶r)"

oops

lemma ejercicio_39:

assumes 1: "p"

shows "¬¬p"

oops

lemma ejercicio_40:

assumes 1: "¬p"

shows "p⟶q"

oops

lemma ejercicio_41:

assumes 1: "p⟶q"

shows "¬q⟶¬p"

oops

lemma ejercicio_42:

assumes 1: "p∨q" and

2: "¬q"

shows "p"

oops

lemma ejercicio_43:

assumes 1: "p∨q" and

2: "¬p"

shows "q"

oops

lemma ejercicio_44:

assumes 1: "p∨q"

shows "¬(¬p∧¬q)"

oops

lemma ejercicio_45:

assumes 1: "p∧q"

shows "¬(¬p∨¬q)"

oops

lemma ejercicio_46:

assumes 1: "¬(p∨q)"

shows "¬p∧¬q"

oops

lemma ejercicio_47:

assumes 1: "¬p∧¬q"

shows "¬(p∨q)"

oops

lemma ejercicio_48:

assumes 1: "¬p∨¬q"

shows "¬(p∧q)"

oops

lemma ejercicio_49:

"¬(p∧¬p)"

oops

lemma ejercicio_50:

assumes 1: "p∧¬p"

shows "q"

oops

lemma ejercicio_51:

assumes 1: "¬¬p"

shows "p"

oops

lemma ejercicio_52:

"p∨¬p"

oops

lemma ejercicio_53:

"((p⟶q)⟶p)⟶p"

oops

lemma ejercicio_54:

assumes 1: "¬q⟶¬p"

shows "p⟶q"

oops

lemma ejercicio_55:

assumes 1: "¬(¬p∧¬q)"

shows "p∨q"

oops

lemma ejercicio_56:

assumes 1: "¬(¬p∨¬q)"

shows "p∧q"

oops

lemma ejercicio_57:

assumes 1: "¬(p∧q)"

shows "¬p∨¬q"

oops

lemma ejercicio_58:

"(p⟶q)∨(q⟶p)"

oops

end

Se puede imprimir o compartir con