Toward a general logicist methodology for engineering ethically correct robots

A general deontic logistic methodology that formalizes moral code allows ethicists to render theories and dilemmas in declarative form for analysis and to engineer ethically correct robots. This methodology is aiming to meet the challenge of ensuring that robot behavior conforms to more general conditions. The method maximizes the probability that a robot behaves in a certifiably ethical fashion in a complex environment that demands such behavior if humans are to be secured. Every meaningful action that the robot performs must access a proof that the action is at least permissible for certifying a behavior to be ethical. A metatheoritical component constitutes a proof theory describing precisely how and when a set of formulas can prove another formula. The logistic methodology allows robots to consult with humans and give humans the power to oversee a robot's reasoning in deliberating about the ethical status of prospective actions.